Parameterized Memory Models and Concurrent Separation Logic

DOI10.1007/978-3-642-11957-6_15MaRDI QIDQ3558227zbMATH OpenOpenAlexFDO

Authors Rodrigo Ferreira, Xinyu Feng, Zhong Shao

Publication date 4 May 2010

Published in Programming Languages and Systems (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-11957-6_15

Mathematics Subject Classification ID

Logic in computer science (03B70) Theory of programming languages (68N15) Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• A formal C memory model for separation logic
• Revisiting concurrent separation logic
• A semantics for concurrent separation logic
• CONCUR 2004 - Concurrency Theory
• Concurrent separation logic and operational semantics
• Separation logic and concurrency
• A promising semantics for relaxed-memory concurrency
• scientific article; zbMATH DE number 3890713

Cited in

(16)

• An axiomatic specification for sequential memory models
• Rely-guarantee bound analysis of parameterized concurrent shared-memory programs. With an application to proving that non-blocking algorithms are bounded lock-free
• A calculus for attribute-based memory updates
• A formal hierarchy of weak memory models
• A separation logic for fictional sequential consistency
• A calculus for relaxed memory
• On Partial Order Semantics for SAT/SMT-Based Symbolic Encodings of Weak Memory Concurrency
• Tackling real-life relaxed concurrency with FSL++
• Granularity and concurrent separation logic
• Observation-based concurrent program logic for relaxed memory consistency models
• Owicki-Gries reasoning for weak memory models
• MSO Logic for Unambiguous Shared-Memory Systems
• Relaxed operational semantics of concurrent programming languages
• A promising semantics for relaxed-memory concurrency
• Operational semantics of a weak memory model with channel synchronization
• Operational semantics of a weak memory model with channel synchronization

This page was built for publication: Parameterized Memory Models and Concurrent Separation Logic

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