Operational semantics of a weak memory model with channel synchronization

DOI10.1016/J.JLAMP.2018.10.004MaRDI QIDQ5915975zbMATH OpenOpenAlexWikidataFDO

Authors Martin Steffen, Volker Stolz, Daniel Schnetzer Fava

Publication date 27 March 2019

Published in Journal of Logical and Algebraic Methods in Programming (Search for Journal in Brave)

Full work available at URL http://hdl.handle.net/10852/61977

zbMATH Keywords

channel communicationdata-race freedom guaranteeoperational semanticsweak memory model

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55)

Recommendations

• Operational semantics of a weak memory model with channel synchronization
• Relaxed memory models
• Relaxed operational semantics of concurrent programming languages
• Parameterized Memory Models and Concurrent Separation Logic
• Studying Operational Models of Relaxed Concurrency

Cites work

• A calculus of mobile processes. II
• A concurrency semantics for relaxed atomics that permits optimisation and avoids thin-air executions
• A promising semantics for relaxed-memory concurrency
• A small-step semantics of a concurrent calculus with Goroutines and deferred functions
• An operational happens-before memory model
• An overview of the K semantic framework
• CakeML
• Can we efficiently check concurrent programs under relaxed memory models in Maude?
• Communicating sequential processes
• Fencing off Go: liveness and safety for channel-based programming
• Generative operational semantics for relaxed memory models
• How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs
• scientific article; zbMATH DE number 41788 (Why is no real title available?)
• scientific article; zbMATH DE number 107700 (Why is no real title available?)
• Is it a ``good encoding of mixed choice?
• Mathematizing C++ concurrency
• Plan B, a buffered memory model for Java
• Relaxed memory models
• Software Transactional Memory on Relaxed Memory Models
• The Java memory model
• Time, clocks, and the ordering of events in a distributed system

Cited in

(3)

• Operational semantics with semicommutations
• On Partial Order Semantics for SAT/SMT-Based Symbolic Encodings of Weak Memory Concurrency
• Operational semantics of a weak memory model with channel synchronization

Describes a project that uses

Uses Software

• K Prover
• CakeML

This page was built for publication: Operational semantics of a weak memory model with channel synchronization

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