锁定的语义规范
编程语言
2015-11-17 v2
摘要
为防止并发错误，程序员需要遵守锁定规范。用于指定该规范的注解（如 Java 的@GuardedBy）已被广泛使用。不幸的是，其语义是以非形式化方式表达的，因此存在歧义。本文强调了此类歧义，并基于类 Java 语言的小型并发片段的操作语义，以两种替代方式形式化了@GuardedBy 的语义。本文还确定了此类注解在何时能真正保证防止数据竞争。我们的工作有助于理解这些注解，并支持开发用于验证或推断此类注解的可靠形式化工具。
引用
@article{arxiv.1501.05338,
title = {Semantics for Locking Specifications},
author = {Michael Ernst and Damiano Macedonio and Massimo Merro and Fausto Spoto},
journal= {arXiv preprint arXiv:1501.05338},
year = {2015}
}