Portal de Periódicos da CAPES

Formal specification and verification of the C ♯ thread model

2005; Elsevier BV; Volume: 343; Issue: 3 Linguagem: Inglês

10.1016/j.tcs.2005.06.028

1879-2294

Robert F. Stärk,

Formal Methods in Verification

We present a high-level Abstract 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.