A semantics for concurrent separation logic

DOI10.1016/J.TCS.2006.12.034zbMATH Open1111.68021OpenAlexW2125398300WikidataQ29396804 ScholiaQ29396804MaRDI QIDQ879367FDOQ879367

Authors: Stephen Brookes 

Publication date: 11 May 2007

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.tcs.2006.12.034

Recommendations

• CONCUR 2004 - Concurrency Theory
• Separation logic and concurrency
• Oracle Semantics for Concurrent Separation Logic
• A grainless semantics for parallel programs with shared mutable data
• A revisionist history of concurrent separation logic

zbMATH Keywords

semanticsconcurrencylogicrace conditionpointers

Mathematics Subject Classification ID

Logic in computer science (03B70) Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Semantics in the theory of computing (68Q55)

Cites Work

• The Logic of Bunched Implications
• Title not available (Why is that?)
• The temporal semantics of concurrent programs
• Full abstraction for a shared-variable parallel language
• Separation and information hiding
• Title not available (Why is that?)
• Verifying properties of parallel programs
• Permission accounting in separation logic
• CONCUR 2004 - Concurrency Theory
• Resources, concurrency, and local reasoning
• Title not available (Why is that?)
• An axiomatic proof technique for parallel programs
• Proofs of Networks of Processes
• Monitors
• Proving Liveness Properties of Concurrent Programs
• The structure of the “THE”-multiprogramming system
• Title not available (Why is that?)
• Title not available (Why is that?)
• Deadlock analysis in networks of communicating processes
• Parallel programming: An axiomatic approach
• Title not available (Why is that?)
• The essence of parallel Algol.
• A hard act to follow
• Local reasoning about a copying garbage collector
• Title not available (Why is that?)
• Title not available (Why is that?)
• A structured paging system

Cited In (84)

• Separation Logic Contracts for a Java-Like Language with Fork/Join
• Title not available (Why is that?)
• Parallelized sequential composition and hardware weak memory models
• Abstract hidden Markov models: a monadic account of quantitative information flow
• Extracting total Amb programs from proofs
• Concurrent Separation Logic Meets Template Games
• Verifying programs with logic and extended proof rules: deep embedding vs. shallow embedding
• Shared contract-obedient endpoints
• Title not available (Why is that?)
• An algebraic glimpse at bunched implications and separation logic
• Step-indexed Kripke model of separation logic for storable locks
• Separation Logic Tutorial
• A fine-grained semantics for arrays and pointers under weak memory models
• A predicate transformer for choreographies. Computing preconditions in choreographic programming
• A first-order logic with frames
• A resource analysis of the \(\pi\)-calculus
• Ownership guided C to Rust translation
• Practical abstractions for automated verification of message passing concurrency
• Verifying a concurrent garbage collector with a rely-guarantee methodology
• Automated theorem proving for assertions in separation logic with all connectives
• A formal semantics of nested atomic sections with thread escape
• Barriers in concurrent separation logic: now with tool support!
• RGITL: a temporal logic framework for compositional reasoning about interleaved programs
• Automatic Parallelization with Separation Logic
• Oracle Semantics for Concurrent Separation Logic
• Automata-theoretic semantics of idealized Algol with passive expressions
• Strict linearizability and abstract atomicity
• An asynchronous soundness theorem for concurrent separation logic
• \textsc{SecCSL}: security concurrent separation logic
• Precision and the conjunction rule in concurrent separation logic
• Pointer race freedom
• On the relation between concurrent separation logic and concurrent Kleene algebra
• Non-preemptive semantics for data-race-free programs
• A revisionist history of concurrent separation logic
• Permission accounting in separation logic
• CONCUR 2004 - Concurrency Theory
• Stone-type dualities for separation logics
• Convolution as a Unifying Concept
• Complexity optimal decision procedure for a propositional dynamic logic with parallel composition
• Elucidating concurrent algorithms via layers of abstraction and reification
• Fifty years of Hoare's logic
• Syntactic control of interference and concurrent separation logic
• Blaming the client: on data refinement in the presence of pointers
• Concurrent separation logic and operational semantics
• Iris from the ground up: a modular foundation for higher-order concurrent separation logic
• Automated verification of parallel nested DFS
• Independence and concurrent separation logic
• A perspective on specifying and verifying concurrent modules
• A separation logic for a promising semantics
• An operational semantics for object-oriented concepts based on the class hierarchy
• Concurrent separation logic for pipelined parallelization
• Improving thread-modular abstract interpretation
• Partition consistency. A case study in modeling systems with weak memory consistency and proving correctness of their implementations
• Barriers in Concurrent Separation Logic
• Separation logic and concurrency
• Parameterized Memory Models and Concurrent Separation Logic
• Modular reasoning about separation of concurrent data structures
• Trace-based verification of imperative programs with I/O
• Separation Logic Semantics for Communicating Processes
• Inter-process buffers in separation logic with rely-guarantee
• Higher-order separation logic in Isabelle/HOLCF
• Fine-grained concurrency with separation logic
• A calculus and logic of bunched resources and processes
• On locality and the exchange law for concurrent processes
• Program logic and equivalence in the presence of garbage collection.
• Communicating state transition systems for fine-grained concurrent resources
• Revisiting concurrent separation logic
• Formal verification of concurrent programs with Read-write locks
• Designing a semantic model for a wide-spectrum language with concurrency
• A discrete geometric model of concurrent program execution
• A grainless semantics for parallel programs with shared mutable data
• Variables as resource for shared-memory programs: semantics and soundness
• Completeness for a first-order abstract separation logic
• A separation logic for refining concurrent objects
• Separation and information hiding
• Local Reasoning for Storable Locks and Threads
• A Formalisation of Smallfoot in HOL
• Type soundness and race freedom for Mezzo
• Reasoning about block-based cloud storage systems via separation logic
• Granularity and concurrent separation logic
• Compositional reasoning
• Interactive proofs in higher-order concurrent separation logic
• Fairness, resources, and separation
• Unified reasoning about robustness properties of symbolic-heap separation logic

This page was built for publication: A semantics for concurrent separation logic

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