Formal specification and verification of the C♯ thread model

We present a high-level State Machine (ASM) model of C♯ threads and the .NET memory model. We focus on purely managed, fully portable threading features of C♯. The sequential model interleaves the computation steps of the currently running threads and is suitable for uniprocessors. The parallel model addresses problems of true concurrency on multi-processor systems. The models provide a sound basis for the development of multi-threaded applications in C♯. The thread and memory models complete the abstract operational semantics of C♯ in [Börger et al. Theoret. Comput. Sci., to appear]. The main invariants of the thread model concerning locks, monitors and mutual exclusion are formally verified in the AsmTP system, an interactive proof assistant based on ASM logic.