Compass: strong and compositional library specifications in relaxed memory separation logic
Hoang-Hai Dang, JaeHwang Jung, Jaemin Choi, Duc-Than Nguyen, William Mansky, Jeehoon Kang, Derek Dreyer
Abstract
Several functional correctness criteria have been proposed for relaxed-memory consistency libraries, but most lack support for modular client reasoning. Mével and Jourdan recently showed that logical atomicity can be used to give strong modular Hoare-style specifications for relaxed libraries, but only for a limited instance in the Multicore OCaml memory model. It has remained unclear if their approach scales to weaker implementations in weaker memory models.
Topics & Concepts
Separation logicAtomicityComputer scienceCorrectnessModular designProgramming languageCompassConsistency (knowledge bases)Sequential consistencyMemory modelConsistency modelTheoretical computer scienceShared memoryParallel computingArtificial intelligenceDatabase transactionCartographyGeographyDistributed systems and fault toleranceParallel Computing and Optimization TechniquesAdvanced Data Storage Technologies