Fine-grained concurrency with separation logic

DOI10.1007/S10992-011-9195-1zbMATH Open1252.03077OpenAlexW2109373243MaRDI QIDQ763473FDOQ763473

Authors: Kalpesh Kapoor, Kamal Lodaya, Uday S. Reddy 

Publication date: 9 March 2012

Published in: Journal of Philosophical Logic (Search for Journal in Brave)

Full work available at URL: http://pure-oai.bham.ac.uk/ws/files/12780883/fine_grained.pdf

Recommendations

• Separation logic and concurrency
• Granularity and concurrent separation logic
• A semantics for concurrent separation logic
• CONCUR 2004 - Concurrency Theory
• A separation logic for refining concurrent objects

zbMATH Keywords

separation logicprogram correctnessgarbage collectionresource logicsconcurrent programsheap storage

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Logic in computer science (03B70) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Cites Work

• The semantics and proof theory of the logic of bunched implications
• The Logic of Bunched Implications
• Title not available (Why is that?)
• BI as an assertion language for mutable data structures
• Linear logic
• A semantics for concurrent separation logic
• An axiomatic basis for computer programming
• Verifying properties of parallel programs
• Permission accounting in separation logic
• Resources, concurrency, and local reasoning
• Concurrency verification. Introduction to compositional and noncompositional methods
• A Marriage of Rely/Guarantee and Separation Logic
• Monitors
• Proving assertions about parallel programs
• Title not available (Why is that?)
• Title not available (Why is that?)
• Modular verification of a non-blocking stack
• On-the-fly garbage collection
• A mechanically verified incremental garbage collector
• Algorithms for on-the-fly garbage collection
• Title not available (Why is that?)
• An exercise in proving parallel programs correct
• Title not available (Why is that?)

Cited In (15)

• Permission-based separation logic for multithreaded Java programs
• Logical reasoning for disjoint permissions
• Logical relations for fine-grained concurrency
• Reasoning over permissions regions in concurrent separation logic
• Permission accounting in separation logic
• Barriers in Concurrent Separation Logic
• Separation logic and concurrency
• Specifying and verifying concurrent algorithms with histories and subjectivity
• Reasoning about optimistic concurrency using a program logic for history
• Permission-based separation logic for message-passing concurrency
• Communicating state transition systems for fine-grained concurrent resources
• Formal verification of concurrent programs with Read-write locks
• A separation logic for refining concurrent objects
• Local Reasoning for Storable Locks and Threads
• Granularity and concurrent separation logic

This page was built for publication: Fine-grained concurrency with separation logic

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