A formal semantics of nested atomic sections with thread escape

DOI10.1016/J.CL.2015.04.001MaRDI QIDQ1749114zbMATH OpenOpenAlexFDO

Authors Frédéric Dabrowski, F. Loulergue, Thomas Pinsard

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

atomicityformal semanticsproof assistantatomic sectionsprogram traceswell-synchronisation

Mathematics Subject Classification ID

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

Recommendations

• A criterion for atomicity
• A semantics for concurrent separation logic
• Meta-analysis for Atomicity Violations under Nested Locking
• AtomCaml: first-class atomicity via rollback
• Publication:4734781

Cites work

• A formal semantics of nested atomic sections with thread escape
• A synthesis of the procedural and declarative styles of interactive theorem proving
• A transactional object calculus
• An introduction to programming and proving with dependent types in Coq
• Coarse-grained transactions
• Formal proof - the four color theorem
• High-level small-step operational semantics for transactions
• 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
• Proving Isolation Properties for Software Transactional Memory
• Semantics of transactional memory and automatic mutual exclusion
• Software transactional memory
• Structural analysis of narratives with the Coq proof assistant
• The calculus of constructions
• The serializability of concurrent database updates

Cited in

(2)

• A formal semantics of nested atomic sections with thread escape
• Partial order and contextual net semantics for atomic and locally atomic CC programs

Describes a project that uses

Uses Software

• miz3
• Coq

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1749114)