A formal semantics of nested atomic sections with thread escape

DOI10.1016/J.CL.2015.04.001zbMath1387.68048OpenAlexW763938970MaRDI QIDQ1749114

Thomas Pinsard, Frédéric Dabrowski, Frédéric Loulergue

Publication date: 15 May 2018

Published in: Computer Languages, Systems \& Structures (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.cl.2015.04.001

zbMATH Keywords

formal semanticsproof assistantatomicityatomic sectionsprogram traceswell-synchronisation

Mathematics Subject Classification ID

Theory of programming languages (68N15) Semantics in the theory of computing (68Q55)

Related Items (1)

A formal semantics of nested atomic sections with thread escape

Uses Software

• Coq
• miz3

Cites Work

• Unnamed Item
• Unnamed Item
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Nested transactional memory: Model and architecture sketches
• The calculus of constructions
• A formal semantics of nested atomic sections with thread escape
• A transactional object calculus
• A Synthesis of the Procedural and Declarative Styles of Interactive Theorem Proving
• Proving Isolation Properties for Software Transactional Memory
• Structural Analysis of Narratives with the Coq Proof Assistant
• High-level small-step operational semantics for transactions
• Semantics of transactional memory and automatic mutual exclusion
• The serializability of concurrent database updates
• Coarse-grained transactions
• Software transactional memory

This page was built for publication: A formal semantics of nested atomic sections with thread escape