/relaxed-memory-separation-logic

Primary LanguageCoqOtherNOASSERTION

A Proof Recipe for Linearizability in Relaxed Memory Separation Logic (COQ DEVELOPMENT)

This is the formalization for the paper "A Proof Recipe for Linearizability in Relaxed Memory Separation Logic," done on top of iRC11 relaxed memory separation logic.

Sunho Park, Jaewoo Kim, Ike Mulder, Jaehwang Jung, Janggun Lee, Robbert Krebbers, and Jeehoon Kang. 2024. A Proof Recipe for Linearizability in Relaxed Memory Separation Logic. Proc. ACM Program. Lang. 8, PLDI, Article 154 (June 2024), 24 pages. https://doi.org/10.1145/3656384

Building on a local machine

This version is known to compile with Coq 8.16.1 and a development version of Iris.

To build it with opam, first install opam with version ≥ 2.1.2, and then run:

opam switch create . ocaml-system --no-install
opam repo add coq-released https://coq.inria.fr/opam/released
opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git
opam pin add -n -y coq 8.16.1

make build-dep

After installing dependencies, run the following to build the entire project.

eval $(opam env)
make -jN # N: number of CPU cores of your machine

It will take some time to compile the entire project. In particular, the compilation of proof_ms_history_diaframe.v may take about one and a half hour, and use about 25GB of memory. You may safely exclude the file from the build by commenting out the line for the file (by inserting # in front) in _CoqProject. In general, every proof file listed in columns OMO and OMO+Diaframe of the table in Case Studies (§6, Table 1) can be excluded from the compilation without causing any dependency problems in compilation.

During the compilation, you might encounter some warning messages like below:

Too little intro patterns were supplied! Please supply a name for:
  x1 : (history tseq_event)
  x2 : omoT
  x3 : (list tseq_state)

Note that these are not compilation errors. Such errors will be notified with explicit error message starting with Error:.

Updating dependencies

Run:

opam update
make build-dep
make clean

Using a provided Docker image

We provide a Docker image, uploaded to zenodo (https://doi.org/10.5281/zenodo.10933398), where the entire project has been already compiled with all dependencies installed. To load the image, first install the Docker engine, and then run:

sudo docker load -i artifact.tar.gz
sudo docker run -it --name artifact artifact:latest

After exiting the container, you can restart it from the loaded image with the following command:

sudo docker run -it --entrypoint=/bin/bash artifact:latest

To rebuild the project, you can clean the project first and then compile it by the following command:

eval $(opam env)
make clean
make -jN # N: number of CPU cores

As mentioned in the section Building on a local machine, compiling the entire project may take some time, and you can safely ignore some proof files without causing any problems.

Case Studies (§6, Table 1)

Object OMO OMO+Diaframe Comparison
Treiber's stack proof_treiber_history.v proof_treiber_history_diaframe.v proof_treiber_history_old.v + spec_history_old.v + event.v1)
Spinlock proof_spin_lock_trylock_history.v proof_spin_lock_trylock_history_diaframe.v lock.v2) (copied version for reproducibility: comparison/lock.v)
Michael-Scott queue proof_ms_history.v proof_ms_history_diaframe.v proof_ms_abs_graph.v + spec_abs_graph.v + queue/spec_graph.v1)
Folly's turn sequencer proof_turnSequencer_composition.v proof_turnSequencer_composition_diaframe.v None
Folly's SPSC queue proof_singleElementQueue_composition.v proof_singleElementQueue_composition_diaframe.v None
Folly's MPMC queue proof_mpmcqueue_composition.v proof_mpmcqueue_composition_diaframe.v None
Exchanger exchanger/proof_composition.v exchanger/proof_composition_diaframe.v proof_graph_piggyback.v + proof_graph_resource.v1)
Elimination stack proof_elim_composition.v proof_elim_composition_diaframe.v proof_elim_graph.v + stack/spec_graph.v + event.v1)
Atomic reference counting (Arc) arc/proof_composition.v None arc_cmra.v + arc.v2) (copied version for reproducibility: comparison/arc_cmra.v, comparison/arc.v)

The line counts in the paper are obtained by counting proof lines of the files specified in the table from Proof. (or Next Obligation.) to Qed. (exclusive), excluding empty lines or comments. These can be counted automatically by using a python script statistics.py.

  1. These proofs are forked from the work by Dang et al.3) but we made some modifications on them. In particular, as we simplified the ORC11 semantics a little (see below for more detail), these proofs became shorter than the original.
  2. Hoang-Hai Dang, Jacques-Henri Jourdan, Jan-Oliver Kaiser, and Derek Dreyer. 2019. RustBelt Meets Relaxed Memory. Proc. ACM Program. Lang. 4, POPL, Article 34 (dec 2019), 29 pages. https://doi.org/10.1145/3371102
  3. Hoang-Hai Dang, Jaehwang Jung, Jaemin Choi, Duc-Than Nguyen, William Mansky, Jeehoon Kang, and Derek Dreyer. 2022. Compass: Strong and Compositional Library Specifications in Relaxed Memory Separation Logic. In Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation (San Diego, CA, USA) (PLDI 2022). Association for Computing Machinery, New York, NY, USA, 792–808. https://doi.org/10.1145/3519939.3523451

Client proofs (§6.6)

Project structure

  1. Hoang-Hai Dang, Jaehwang Jung, Jaemin Choi, Duc-Than Nguyen, William Mansky, Jeehoon Kang, and Derek Dreyer. 2022. Compass: Strong and Compositional Library Specifications in Relaxed Memory Separation Logic. In Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation (San Diego, CA, USA) (PLDI 2022). Association for Computing Machinery, New York, NY, USA, 792–808. https://doi.org/10.1145/3519939.3523451

Object Modification Order (OMO) Library (§3, §4)

The table below describes how the important concepts in our paper are modeled in this repository.

Paper Coq
OMO has a type of list (list EventId). OMO is a list of a pair of a write event and a list of read-only events, denoted by list (event_id * list event_id). This enforces each generation has write event.
Event history H is a mapping from EventId to Event(T) where T is a type of event. Event history E is a list of events which has type omo_event T where each event is ordered in execution order.
Event(T) is a record of type, sync-view, eview. omo_event T is a record of type, sync-view, eview, which directly matches with the Event(T).
EventId is an abstract type. event_id is a natural number denoting an index of each event in the event history E.
Object's sequential specification is given as a tuple (T, S, σ₀, →). Object's sequential specification is given as the Interpretable T S typeclass which contains init (initial state, σ₀) and step (state transition, →).

The table below compares the definitions and predicates used in the paper with those in the Coq mechanization.

Paper Coq Note
OmoAuth(γₒ,γₛ,H,omo,Σ) OmoAuth γₒ γₛ q E omo Σ q denotes fractional ownership which allows splitting ownership of OmoAuth.
⊒γoM OmoEview γₒ M
OmoSnap(γₒ,γₛ,e,σ) OmoSnap γₒ γₛ e σ
interpomo(H,omo,σ₀,Σ) interp_omo E omo σ₀ Σ Encoded in Linearizability_omo, a predicate for well-formedness of OMO structure guaranteed by OmoAuth.
lhb(H,π) lhb E lin lin is a list of event id, in contrast to π being a permutation.
lhbomo(H,omo) lhb_omo E omo Encoded in Linearizability_omo, a predicate for well-formedness of OMO structure guaranteed by OmoAuth.
Token(γₒ,e) OmoToken(R|W) γₒ e OmoTokenR corresponds to Tokenr and OmoTokenW corresponds to Tokenw (§5).
maxGen(omo,M) ≤ n OmoUBgen omo M n OmoUB is vProp version of OmoUBgen where comparison of generations is asserted by OmoLe predicates.
commit-with relation from e (γₒ) to e' (γₒ') OmoCW γₒ γₒ' e e'
OMO points-to predicate append_only_loc + OmoAuth + (swriter_token) Supports two protocols that ensure append-only properties (no insertion of write event in the middle): single writer, cas-only.
LocSeen ℓ γₒ M OmoEview γₒ M
Omo≤(γₒ,e,e') OmoLe γₒ e e' Similar predicates OmoEq, OmoLt are also provided.
CWMono(γₒ,H) CWMono γₒ γₒ' γₘ M Coq version asserts monotonicity for all commit-with relations with upper-level events in M between upper-level (γₒ) and lower-level (γₒ') objects. γₘ is a ghost name for the ghost set on M.

The table below highlights the locations of important lemmas.

Rule File Lemma
OmoAuth-Linearizable omo_preds.v OmoAuth_Linearizable1)
Omo-Compatible omo.v omo_compatible
OmoSnap-Get omo_preds.v OmoSnap_get
OmoAuth-OmoSnap omo_preds.v OmoAuth_OmoSnap
OmoAuth-Alloc omo_preds.v OmoAuth_alloc
OmoAuth-Insert-Ro omo_preds.v OmoAuth_insert_ro_gen (OmoAuth_insert_ro is also used often)
OmoAuth-Insert-Last omo_preds.v OmoAuth_insert_last
OmoAuth-Insert omo_preds.v OmoAuth_insert
Omo-Points-To-Alloc append_only_loc.v append_only_loc_(cas_only|swriter)_from_na2)
Omo-Points-To-Load append_only_loc.v append_only_loc_read2)
Omo-Points-To-Store append_only_loc.v append_only_loc_write2)
Omo-Points-To-CAS append_only_loc.v append_only_loc_cas_general2)
OmoLe-Get omo_preds.v OmoLe_get
OmoLe-Le omo_preds.v OmoLe_Le
  1. Definition of Linearizability_omo used in the lemma OmoAuth_Linearizable can be found in omo.v. Note that the definition of Linearizability_omo directly matches with conclusion of the rule in the paper.
  2. In the paper, composable linearizability specification for shared location strictly follows the style of the specification by encoding semantics of memory accesses with abstract state transitions. The rules in Coq, instead expose the semantics explicitly in the specification. This helps simplify the proof process. Note that, both encodings are equivalent.

Stack predicates in paper (Fig. 8) and in Coq have some differences. Notable ones are:

  • Coq version starts with the meta predicate, which persistently associates a location to a list of values, while the paper version simply omitted such detail.
  • PhysList in the paper corresponds to StackNodes in Coq. While PhysList is asserted for every location event, StackNodes is asserted only for the latest write event, which is sufficient and more convenient to establish the invariant. Note that although paper version uses persistent points-to assertion (↦□), Coq version does not use it. Instead, we mimic the characteristic of persistency by taking out fractional ownership of points-to assertion from PhysList and keeping it in the proof context for later use of read operations.
  • The ∀-quantified part in the paper corresponds to AllLinks in Coq. While the paper version maintains it for all location events, the Coq version maintains it only for all write events of a location, which also simplifies the proof.
  • Stk3 asserted in SeenStack in the paper corresponds to seen_event_info in Coq. It uses the OmoHb predicate, which is a generalization of Stk3 but only in one-direction: observation of a upper-level object event implies observation of lower-level object event.
  • CWMono in the paper corresponds to CWMono in Coq.

Diaframe Automation (§5)

We construted a hint database for Diaframe to extend it into RMC separation logic and to make it usable with OMO predicates and rules. The interesting files are as follows:

  • view_hints.v: hints for handling view-at modality (§5.2, in particular the idea of 'applying VA-Intro rule whenever possible' is represented by the hints mergable_consume_always_intro_view_at_first and mergable_consume_always_intro_view_at_step).
  • omo_hints.v: hints for automating proofs using the OMO library (§5.3).
  • omo_specs.v: special hints for automatic symbolic execution for proofs using the using OMO points-to predicates (§5.3).
  • base_hints.v: general hints for Diaframe (related to §5.3, in particular hints for ask_for mechanism are written in this file).

Below, we briefly explain several useful tactics. For more information, please refer to the repository of Diaframe.

  • iStep, iSteps: These are main tactics provided by Diaframe. It takes multiple automatic steps based on primitive rules of Diaframe and Diaframe hints. iStep performs a single chunk of automation step, while iSteps repeats iStep whenever possible.
  • iStepSafest, iStepsSafest: These tactics are more conservative then iStep and iSteps in the sense that former ones stop when a goal is a disjunction. As previous, iStepsSafest repeats iStepSafest whenever possible.
  • iStepDebug, solveStep: These are for debugging steps. iStepDebug turns current goal into the form that Diaframe can understand, and solveStep takes a single basic step, which is much smaller than the step that iStep takes.
  • oSteps: This is a tactic defined by our work (see its definition in omo_hints.v). It automatically applies a collection of rewrite rules that are widely used in our recipe while repeatedly performing iStepsSafest.

Change in Semantics

This project is built upon iRC11, a separation logic for the ORC11 memory model. For better support for automation, we simplified the semantics of ORC11 that does not change the core part of the memory model, explained below. Note that we did not touch the race detector of ORC11.