Semantics for Locking Specifications

被引：1
作者：
Ernst, Michael D. [1 ]
Macedonio, Damiano [2 ]
Merro, Massimo [2 ]
Spoto, Fausto [2 ]
机构：
[1] Univ Washington, Comp Sci & Engn, Seattle, WA 98195 USA
[2] Univ Verona, Dipartimento Informat, Verona, Italy
来源：
NASA FORMAL METHODS, NFM 2016 | 2016年 / 9690卷
关键词：
!text type='JAVA']JAVA[!/text;
D O I：
10.1007/978-3-319-40648-0_27
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
Lock-based synchronization disciplines, like Java's @GuardedBy, are widely used to prevent concurrency errors. However, their semantics is often expressed informally and is consequently ambiguous. This article highlights such ambiguities and overcomes them by formalizing two possible semantics of @GuardedBy, using a reference operational semantics for a core calculus of a concurrent Java-like language. It also identifies when such annotations are actual guarantees against data races. Our work aids in understanding the annotations and supports the development of sound tools that verify or infer them.
引用
收藏
页码：355 / 372
页数：18
相关论文
共 18 条
  • [1] Types for safe locking: Static race detection for Java']Java
    Abadi, M
    Flanagan, C
    Freund, SN
    [J]. ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 2006, 28 (02): : 207 - 255
  • [2] Abrahám-Mumm E, 2002, LECT NOTES COMPUT SC, V2303, P5
  • [3] Bierman G. M., 2003, ENTCS, V82, P82, DOI DOI 10.1016/S1571-0661(04)80803-X
  • [4] Escape analysis for Java']Java™:: Theory and practice
    Blanchet, B
    [J]. ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 2003, 25 (06): : 713 - 775
  • [5] Bogdanas D, 2015, ACM SIGPLAN NOTICES, V50, P445, DOI [10.1145/2775051.2676982, 10.1145/2676726.2676982]
  • [6] Cenciarelli P., 1997, Algebraic Methodology and Software Technology. 6th International Conference, AMAST '97. Proceedings, P75, DOI 10.1007/BFb0000464
  • [7] Dietl W., 2011, ICSE 2011
  • [8] Ernst M., 2016, ICSE 2016
  • [9] Ernst M. D., 2015, ABS150105338 CORR
  • [10] Goetz B., 2006, Java Concurrency in Practice
12