SyncGen: an aspect-oriented framework for synchronization This paper describes SyncGen – a tool for automatically synthesizing complex synchronization implementations from formal high-level specifications. In SyncGen, synchronization specifications are phrased using first-order logic or user-friendly specification patterns. From a high-level specification, a language independent synchronization solution in an intermediate guarded-command language is synthesized. Back-end translators can translate this intermediate solution into a variety of implementation frameworks including Java, C++/C with POSIX threads, and Controller Area Network message passing primitives. SyncGen has been used extensively in courses at Kansas State University. Its breadth of applicability has been demonstrated by using it to solve virtually all of the exercises given in well-known concurrency textbooks, as well as a variety of real-world problems in the embedded computing domain. The tool, along with supporting documentation and an example repository, is publicly available.
Keywords for this software
References in zbMATH (referenced in 7 articles , 1 standard article )
Showing results 1 to 7 of 7.
- Deshmukh, Jyotirmoy; Ramalingam, G.; Ranganath, Venkatesh-Prasad; Vaswani, Kapil: Logical concurrency control from sequential proofs (2011)
- Emerson, E.Allen; Samanta, Roopsha: An algorithmic framework for synthesis of concurrent programs (2011)
- Flanagan, Cormac; Freund, Stephen N.: Atomizer: A dynamic atomicity checker for multithreaded programs (2008)
- Betin-Can, Aysu; Bultan, Tevfik: Highly dependable concurrent programming using design for verification (2007)
- Iosif, Radu; Dwyer, Matthew B.; Hatcliff, John: Translating Java for multiple model checkers: The Bandera back-end (2005)
- Deng, Xianghua; Dwyer, Matthew B.; Hatcliff, John; Mizuno, Masaaki: SyncGen: an aspect-oriented framework for synchronization (2004)
- Betin-Can, Aysu; Bultan, Tevfik: Interface-based specification and verification of concurrency controllers. (2003)