In this project, we will develop techniques and tools for specifying TM and verifying TM implementations. We will first consider the issue of defining TM as an additional synchronization primitive in object-oriented imperative programming languages. For different major categories of TMs integrated into programming languages, we will devise programming-language-level semantics.
We will also identify the assumptions the TM specification must make on the TM implementation in order to guarantee desired correctness properties at the semantics level. Under these assumptions, we will verify that the TM satisfies the desired properties using a static verification tool that we will develop for this purpose. In the second phase of the proof effort, again using the static verification tool, we will prove that the assumptions made at the algorithm level are satisfied by the TM implementation source code.
This low-level proof effort will be carried out twice, once for each major category of TM algorithms. In the final phase of the project, we will concentrate on modularizing the static proof approach, and incorporating weak (relaxed) memory models into the proof system and tool.