Verifying correct usage of atomic blocks and typestate Export

@inproceedings{citeulike:5793650, abstract = {The atomic block, a synchronization primitive provided to programmers in transactional memory systems, has the potential to greatly ease the development of concurrent software. However, atomic blocks can still be used incorrectly, and race conditions can still occur at the level of application logic. In this paper, we present a intraprocedural static analysis, formalized as a type system and proven sound, that helps programmers use atomic blocks correctly. Using access permissions , which describe how objects are aliased and modified, our system statically prevents race conditions and enforces typestate properties in concurrent programs. We have implemented a prototype static analysis for the Java language based on our system and have used it to verify several realistic examples.}, address = {New York, NY, USA}, author = {Beckman, Nels E. and Bierhoff, Kevin and Aldrich, Jonathan}, booktitle = {OOPSLA '08: Proceedings of the 23rd ACM SIGPLAN conference on Object-oriented programming systems languages and applications}, citeulike-article-id = {5793650}, citeulike-linkout-0 = {http://portal.acm.org/citation.cfm?id=1449764.1449783}, citeulike-linkout-1 = {http://dx.doi.org/10.1145/1449764.1449783}, doi = {10.1145/1449764.1449783}, isbn = {978-1-60558-215-3}, keywords = {concurrency, pl, substructural}, location = {Nashville, TN, USA}, pages = {227--244}, posted-at = {2009-09-17 00:30:05}, priority = {3}, publisher = {ACM}, title = {Verifying correct usage of atomic blocks and typestate}, url = {http://dx.doi.org/10.1145/1449764.1449783}, year = {2008} }

TY - CONF ID - citeulike:5793650 L3 - citeulike-article-id:5793650 N2 - The atomic block, a synchronization primitive provided to programmers in transactional memory systems, has the potential to greatly ease the development of concurrent software. However, atomic blocks can still be used incorrectly, and race conditions can still occur at the level of application logic. In this paper, we present a intraprocedural static analysis, formalized as a type system and proven sound, that helps programmers use atomic blocks correctly. Using access permissions , which describe how objects are aliased and modified, our system statically prevents race conditions and enforces typestate properties in concurrent programs. We have implemented a prototype static analysis for the Java language based on our system and have used it to verify several realistic examples. CY - Nashville, TN, USA SN - 978-1-60558-215-3 AD - New York, NY, USA EP - 244 TI - Verifying correct usage of atomic blocks and typestate PB - ACM T2 - OOPSLA '08: Proceedings of the 23rd ACM SIGPLAN conference on Object-oriented programming systems languages and applications SP - 227 KW - concurrency KW - pl KW - substructural AU - Beckman, Nels AU - Bierhoff, Kevin AU - Aldrich, Jonathan PY - 2008/// UR - http://dx.doi.org/10.1145/1449764.1449783 ER -