The JCert team is an international collaboration between Inria – Celtique team and Purdue University.
Safety-critical applications demand rigorous, unambiguous guarantees on program correctness. While a combination of testing and manual inspection is typically used for this purpose, bugs latent in other components of the software stack, especially the compiler and the runtime system, can invalidate these hard-won guarantees. To address such concerns, additional laborious techniques such as manual code reviews of generated assembly code are required by certification agencies. Significant restrictions are imposed on compiler optimizations that can be performed, and the scope of runtime and operating system services that can be utilized. To alleviate this burden, the JCert project would like to implement a verified compiler and runtime for managed concurrent languages similar to Java or C#.
This goal is a challenging and ambitious one for several reasons. Besides the well-known challenges to verification that application-level concurrency introduces, components of the implementation may also run concurrently with application threads, improving scalability and performance, at the cost of additional complexity. The interaction among components is typically regulated by compiler-injected code that maintains and updates information useful to the runtime system during program execution. Examples of such code include handlers for memory allocation fast paths, read and write barriers for memory management, fences, etc. These concurrent snippets are sophisticated, can be racy, and must operate correctly in an environment subject to program transformations, both local and global. Equally challenging is understanding the correctness of translations in the presence of subtle visibility rules on shared-memory updates and accesses (i.e., the language memory model). Indeed, the complexity and interactions of these issues precludes the use of brute-force reasoning, and requires incorporating new proof techniques and methodologies to advance the state-of-the-art.
- David Pichardie (scientific leader)
- Jan Vitek
- Gustavo Petri
- Thomas Jensen
- Delphine Demange
- Vincent Laporte
|||Suresh Jagannathan, Vincent Laporte, Gustavo Petri, David Pichardie, and Jan Vitek. Atomicity refinement for verified compilation. ACM Trans. Program. Lang. Syst. (TOPLAS), 36(2):1, 2014. [ bib | .pdf | Abstract ]|
|||Suresh Jagannathan, Vincent Laporte, Gustavo Petri, David Pichardie, and Jan Vitek. Atomicity refinement for verified compilation. In ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI’14, page 5. ACM, 2014. Submitted and accepted to TOPLAS vol 36, presented at PLDI the same year. [ bib | .pdf | Abstract ]|