A denotational semantics for SPARC TSO

DOI10.1016/J.ENTCS.2018.03.025OpenAlexW2964334533WikidataQ113317555 ScholiaQ113317555MaRDI QIDQ2130595

Stephen Brookes, Ryan Kavanagh

Publication date: 25 April 2022

Full work available at URL: https://doi.org/10.1016/j.entcs.2018.03.025

zbMATH Keywords

denotational semanticsconcurrencyweak memory modelspomsetsSPARC TSO

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (4)

Modular Relaxed Dependencies in Weak Memory Concurrency ⋮ Trace semantics and algebraic laws for MCA ARMv8 architecture based on UTP ⋮ Parallelized sequential composition and hardware weak memory models ⋮ An algebraic theory for shared-state concurrency

Cites Work

• Modeling concurrency with partial orders
• Full abstraction for a shared-variable parallel language
• Brookes Is Relaxed, Almost!
• How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs
• Time, clocks, and the ordering of events in a distributed system
• Relaxed memory models
• Mathematizing C++ concurrency

This page was built for publication: A denotational semantics for SPARC TSO