The verification of concurrent program correctness poses intricate challenges due to the non-deterministic nature of concurrent execution. In such scenarios, multiple threads or processes interact with shared resources, and the scheduling of operations yields varying interleavings, rendering program behavior non-deterministic. Our research is geared towards advancing the verification of concurrent program correctness. One facet of our work centers on formally verifying the atomic execu- tion of programs post-compilation into lock-based constructs within a sequentially consistent memory setting. Another aspect focuses on enhancing the correctness of software transactional memory. To tackle these issues, we establish two comprehen- sive frameworks from the ground up, utilizing the HOL theorem prover. One framework accommodates both lock-based and atomic program constructs through an abstract model encompassing a heap, store, and program commands. After establishing fundamental definitions, we engage in a verification process that assesses framework correctness, including separation logic rules and parallel compo- sition. Further fortifying its reliability, we verify the in-place list reversal algorithm. To ensure accurate compilation of atomic programs into lock-based counterparts, we introduce a translation function capturing this conversion process. Our work ex- tends to verifying compilation for non-deterministic concurrent programs, exploring the preservation of target behaviors when the source executes and vice versa.

The second framework is about formally mechanizing software transactions and their corresponding histories, serving as a cornerstone for formal proofs. Amidst varying interpretations of correctness in Software Transactional Memory (STM), opac- ity holds significance, extending the notion of strict serializability from database transactions. Our analysis critically evaluates Guerraoui et al.’s initial work in STM correctness, particularly their reduction theorem for strict serializability and opac- ity. We identify limitations in their approach, leading us to propose new definitions and proofs. Consequently, we formulate a fresh reduction theorem for opacity, sup- ported by a set of properties facilitating its proof. Our research collectively enriches the landscape of concurrent program verification and STM correctness.