Abstract local reasoning for concurrent libraries: mind the gap

DOI10.1016/J.ENTCS.2014.10.009MaRDI QIDQ283756zbMATH OpenOpenAlexWikidataFDO

Authors Philippa Gardner, Azalea Raad, Mark Wheelhouse, Adam Wright

Publication date 13 May 2016

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

zbMATH Keywords

abstractionconcurrencyrefinementseparationreasoningtranslation

Mathematics Subject Classification ID

Data structures (68P05) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Logic in computer science (03B70) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Programming Languages and Systems
• Locally abstract, globally concrete semantics of concurrent programming languages
• Resources, concurrency, and local reasoning
• Elucidating concurrent algorithms via layers of abstraction and reification
• CONCUR 2004 - Concurrency Theory
• Local Reasoning for Storable Locks and Threads
• Reverse exchange for concurrency and local reasoning

Cites work

• Abstract local reasoning for concurrent libraries: mind the gap
• Blaming the client: on data refinement in the presence of pointers
• Context logic and tree update
• Fictional separation logic
• Impredicative concurrent abstract predicates
• Local Reasoning for the POSIX File System
• Permission accounting in separation logic
• Resources, concurrency, and local reasoning
• Unifying refinement and Hoare-style reasoning in a logic for higher-order concurrency
• Variables as resource in separation logic
• Views, compositional reasoning for concurrent programs

Cited in

(4)

• Thread-Local Semantics and Its Efficient Sequential Abstractions for Race-Free Programs
• Programming Languages and Systems
• Abstract local reasoning for concurrent libraries: mind the gap
• DOM: Specification and Client Reasoning

This page was built for publication: Abstract local reasoning for concurrent libraries: mind the gap

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