@@ -17,9 +17,9 @@ Install the requirements of this project using
opam install . --deps-only -j <NUMBEROFJOBS>
After this you should be able to use `make` to compile the various examples, which are located in `theories/examples/comparison`:
-`make test`: verifies a spin lock, CLH lock and an ARC
-`make rwlocks`: verifies 4 reader-writer locks in `theories/examples/comparison`
After this you should be able to use `make` to compile the various examples, which are located in [theories/examples/comparison](./theories/examples/comparison):
-`make test`: verifies a spin lock, CLH lock and an ARC.
-`make rwlocks`: verifies the 4 different reader-writer locks.
-`make comparison-quick`: verifies 17/24 examples: those which verify relatively quickly.
-`make comparison`: verifies 21/24 examples: verifies 4 additional examples, which take ~2 minute per example. `make comparison` should take about 12-20 minutes on a single core
-`make comparison-all`: verifies all examples. Beware, this takes a while (~40 minutes on a single core).
...
...
@@ -31,7 +31,7 @@ First you need to clone the projects in their relevant `external/` folders using
git submodule update --init --recursive
After this you should be able to use `make` to compile the examples:
-`make actris`: verifies the parallel map implementation provided be Actris, using the automation of this project
-`make actris`: verifies the parallel map implementation provided by Actris, using the automation of this project
-`make reloc`: verifies that a ticket lock refines a spin lock, and that a fine-grained stack refines a course-grained stack, using the automation of this project.
## Generating the statistics table
...
...
@@ -42,68 +42,68 @@ Next, run `python utils/stats_gen.py` from the root of the project. See `python
## Directory structure
All Coq files reside in (subdirectories of) the `theories/` folder.
All Coq files reside in (subdirectories of) the [theories](./theories) folder.
#### Files in `theories/`
#### Files in [theories](./theories)
These files contain definitions and utilities used throughout the project
-`solve_defs.v`: Defines the hint formats `BiAbd` and `Abduct` and the goal formats `SolveSep` and `SolveOne`
-`util_classes.v`: Defines several typeclasses used throughout the project. An important ones is `ModalityEC`. Roughly speaking, if `ModalityEC M` is true, and we can `SplitModality3 M ?M1 ?M2` the proof-search strategy works behind modality `M`.
-`util_instances.v`: Contains instances of typeclasses defined above
-`env_utils.v`: Contains some additional lemmas for manipulating IPM's environments
-`tele_utils.v`: Contains machinery and lemmas to be able to work under existentials, and to be able to separate relevant from irrelevant existentials.
#### Files in `theories/hint_search`
-[solve_defs.v](./theories/solve_defs.v): Defines the hint formats `BiAbd` and `Abduct` and the goal formats `SolveSep` and `SolveOne`
-[util_classes.v](./theories/util_classes.v): Defines several typeclasses used throughout the project. An important ones is `ModalityEC`. Roughly speaking, if `ModalityEC M` is true, and we can `SplitModality3 M ?M1 ?M2` the proof-search strategy works behind modality `M`.
-[util_instances.v](./theories/util_instances.v): Contains instances of typeclasses defined above
-[env_utils.v](./theories/env_utils.v): Contains some additional lemmas for manipulating IPM's environments
-[tele_utils.v](./theories/tele_utils.v): Contains machinery and lemmas to be able to work under existentials, and to be able to separate relevant from irrelevant existentials.
#### Files in [theories/hint_search](./theories/hint_search)
These files are all related to the (bi-)abduction hints
-`lemmas_biabd.v`: Contains proofs of all recursive rules for constructing bi-abduction hints.
-`lemmas_abd.v`: Contains proofs of all recursive rules for constructing abduction hints.
-`search_biabd.v`: Defines the search procedure for bi-abduction hints, using the recursive rules.
-`search_abd.v`: Defines the search procedure for abduction hints, using the recursive rules.
-`instances_base.v`: Defines the base hint instances, also for Iris.
-`explicit_hint_registration.v`: Defines a way to reset the registered hints, so the number of distinct hints used can be counted.
#### Files in `theories/steps`
-[lemmas_biabd.v](./theories/hint_search/lemmas_biabd.v): Contains proofs of all recursive rules for constructing bi-abduction hints.
-[lemmas_abd.v](./theories/hint_search/lemmas_abd.v): Contains proofs of all recursive rules for constructing abduction hints.
-[search_biabd.v](./theories/hint_search/search_biabd.v): Defines the search procedure for bi-abduction hints, using the recursive rules.
-[search_abd.v](./theories/hint_search/search_abd.v): Defines the search procedure for abduction hints, using the recursive rules.
-[instances_base.v](./theories/hint_search/instances_base.v): Defines the base hint instances necessary for minimum functionality.
-[explicit_hint_registration.v](./theories/hint_search/explicit_hint_registration.v): Defines a way to reset the registered hints, so the number of distinct hints used can be counted.
#### Files in [theories/steps](./theories/steps)
These files contain the proofs and tactics for executing the proof-search strategy.
-`solve_sep.v`: Contains lemmas and tactics for making progress on `Δ ⊢ || M || ∃ x, A ∗ G` goals (`SolveSep` goals). In particular, contains the proof of the application of bi-abduction hints.
-`solve_one.v`: Contains lemmas and tactics for making progress on `Δ ⊢ M (∃ x, A)` goals (`SolveOne` goals). In particular,
-[solve_sep.v](./theories/steps/solve_sep.v): Contains lemmas and tactics for making progress on `Δ ⊢ || M || ∃ x, A ∗ G` goals (`SolveSep` goals). In particular, contains the proof of the application of bi-abduction hints.
-[solve_one.v](./theories/steps/solve_one.v): Contains lemmas and tactics for making progress on `Δ ⊢ M (∃ x, A)` goals (`SolveOne` goals). In particular,
contains the proof of the application of abduction hints.
-`introduce_hyp.v`: Contains lemmas and tactis for making progress on `Δ ⊢ U -∗ G` goals (`IntroduceHyp` goals). This file is responsible for decomposing `U`s into `H_C`s, and for finding interference between hypotheses (i.e. `MergablePersist` or `MergableConsume` instances).
-`introduce_var.v`: Contains lemmas and tactics for making progress on `Δ ⊢ ∀ x. G x` goals (`IntroduceVars` goals). Quite short, no special things happen here.
-`merge_mod.v`: Contains lemmas and tactics for making progress on `Δ ⊢ ⊳ G` goals (`MergeMod` goals). Works for general `IntroducableModality`s, in practice only used for `⊳`. Responsible for making sure laters get stripped of hypotheses when the goal contains a later.
-`solve_instances.v`: Contains some additional typeclass instances necessary for using Diaframe's automation.
-`pure_solver.v`: Defines the pure solver used in various places throughout the project.
-`small_steps.v`: Combines the lemmas and tactics from this folder to construct the `solveSteps` tactic, which runs the proof-search strategy as long as the goals are `SolveSep`, `SolveOne`, `IntroduceHyp`, `IntroduceVars` or `MergeMod`. In this way, it ensures we can run the proof-search strategy to execute a single statement, without observing all tiny steps in between. This is useful for debugging and using the strategy in interactive mode.
-`tactics.v`: Uses the `solveSteps` tactic from `small_steps.v` to build the `iStepS` and `iStepsS` tactics. `iStepS` turns the goal into one of `SolveSep`, `SolveOne`, `IntroduceHyp`, `IntroduceVars` or `MergeMod`, then runs `solveSteps`. `iStepsS` roughly repeatedly calls `iStepS`, and thus runs the proof-search strategy continuously. This file contains some additional instances that make raw `solveStep` goals work better in interactive Iris proofs.
-`verify_tac.v`: Uses `iStepsS` to build `verify_tac`. This basically does Löb induction, then runs `iStepsS`. If this stops before finishing, it tries to run `lang_open_tac` to *once* unfold a recursive program. It then runs `iStepsS` again. As we are mainly verifying tail-recursive programs, this strategy works most of the time.
-[introduce_hyp.v](./theories/steps/introduce_hyp.v): Contains lemmas and tactis for making progress on `Δ ⊢ U -∗ G` goals (`IntroduceHyp` goals). This file is responsible for decomposing `U`s into `H_C`s, and for finding interference between hypotheses (i.e. `MergablePersist` or `MergableConsume` instances).
-[introduce_var.v](./theories/steps/introduce_var.v): Contains lemmas and tactics for making progress on `Δ ⊢ ∀ x. G x` goals (`IntroduceVars` goals). Quite short, no special things happen here.
-[merge_mod.v](./theories/steps/merge_mod.v): Contains lemmas and tactics for making progress on `Δ ⊢ ⊳ G` goals (`MergeMod` goals). Works for general `IntroducableModality`s, in practice only used for `⊳`. Responsible for making sure laters get stripped of hypotheses when the goal contains a later.
-[solve_instances.v](./theories/steps/solve_instances.v): Contains some additional typeclass instances necessary for using Diaframe's automation.
-[pure_solver.v](./theories/steps/pure_solver.v): Defines the pure solver used in various places throughout the project.
-[small_steps.v](./theories/steps/small_steps.v): Combines the lemmas and tactics from this folder to construct the `solveSteps` tactic, which runs the proof-search strategy as long as the goals are `SolveSep`, `SolveOne`, `IntroduceHyp`, `IntroduceVars` or `MergeMod`. In this way, it ensures we can run the proof-search strategy to execute a single statement, without observing all tiny steps in between. This is useful for debugging and using the strategy in interactive mode.
-[tactics.v](./theories/steps/tactics.v): Uses the `solveSteps` tactic from `small_steps.v` to build the `iStepS` and `iStepsS` tactics. `iStepS` turns the goal into one of `SolveSep`, `SolveOne`, `IntroduceHyp`, `IntroduceVars` or `MergeMod`, then runs `solveSteps`. `iStepsS` roughly repeatedly calls `iStepS`, and thus runs the proof-search strategy continuously. This file contains some additional instances that make raw `solveStep` goals work better in interactive Iris proofs.
-[verify_tac.v](./theories/steps/verify_tac.v): Uses `iStepsS` to build `verify_tac`. This basically does Löb induction, then runs `iStepsS`. If this stops before finishing, it tries to run `lang_open_tac` to *once* unfold a recursive program. It then runs `iStepsS` again. As we are mainly verifying tail-recursive programs, this strategy works most of the time.
The files below are also in this folder, but less relevant:
-`local_post.v`: a tactic which can be used to add a form of ''proof outlines'' to an Iris proof. Used in the `barrier` and `peterson` example, mainly useful for reducing number of goals to prove if there are a lot of disjunctions.
-`namer_tacs.v`: an interface which can be used to provide better names for automatically introduced hypotheses.
#### Files in `theories/symb_exec`
-[local_post.v](./theories/steps/local_post.v): a tactic which can be used to add a form of ''proof outlines'' to an Iris proof. Used in the `barrier` and `peterson` example, mainly useful for reducing number of goals to prove if there are a lot of disjunctions.
-[namer_tacs.v](./theories/steps/namer_tacs.v): an interface which can be used to provide better names for automatically introduced hypotheses.
#### Files in [theories/symb_exec](./theories/symb_exec)
This folder contains some infrastructure for generic assertions that can ''execute'', like WP. This is not discussed in the paper.
-`defs.v`: contains definitions of a generic ''ExecuteOp''.
-`weakestpre.v`: contains an instantiation of this for WP.
-`spec_notation.v`: defines the `SPEC` notation, in terms of a `ReductionStep` defined in `defs.v`. Comes with an `unfold_spec_goal`, which unfolds a `SPEC` goals into one using just `WP`s.
#### Files in `theories/libs`
-[defs.v](./theories/symb_exec/defs.v): contains definitions of a generic ''ExecuteOp''.
-[weakestpre.v](./theories/symb_exec/weakestpre.v): contains an instantiation of this for WP.
-[spec_notation.v](./theories/symb_exec/spec_notation.v): defines the `SPEC` notation, in terms of a `ReductionStep` defined in `defs.v`. Comes with an `unfold_spec_goal`, which unfolds a `SPEC` goals into one using just `WP`s.
#### Files in [theories/lib](./theories/lib)
This folder defines several ghost-state and hint libraries used in different examples.
-`ticket_cmra.v`: basically a wrapper around the `CoPset` cmra, that separates singletons and the set of all numbers below/under a given one. Used in the `ticket_lock` and the `barrier` examples.
-`frac_token.v`: Defines the `token`, `no_tokens` and `token_counter` resources from the ARC example. Actually defined on top of:
-`tokenizable.v`: More abstract version of above, does not constrain `token`s to only work for Fractionals.
-`Z_cmra.v`: Instantiates the integers `Z` with addition as a cmra. The `≼` operation is trivial on these
-`int_as_nat_diff.v`: It is sometimes useful to represent `Z` as the difference between two (rising) natural numbers. This file extends the pure automation with such a concept. Used in `rwlock_linux_bounded` and the `inc_dec` counter.
-`loc_map.v`: It is sometimes useful to be able to couple locations to specific data (often `gname`s). This file makes that doable without much hassle.
-`except_zero.v`: Makes Diaframe strip off the except zero modality when possible when introducing hypotheses. Additionally, makes Diaframe strip off laters of Timeless hypotheses.
-`persistently.v`: Adds support for proving goals behind a `<pers>` modality.
-`intuitionistically.v`: Adds support for proving goals behind a `□` modality.
-`iris_hints.v`: Adds hints specific to Iris's logic - rules for manipulating invariants.
-`own_hints.v`: Adds hints for working with `own γ a` hypotheses, where `a` is a ghost element built from Iris's cmra building blocks (like `auth`, `agree`, `prod`, `option`, `excl`, etcetera.).
#### Files in `theories/heap_lang`
-[ticket_cmra.v](./theories/lib/ticket_cmra.v): basically a wrapper around the `CoPset` cmra, that separates singletons and the set of all numbers below/under a given one. Used in the `ticket_lock` and the `barrier` examples.
-[frac_token.v](./theories/lib/frac_token.v): Defines the `token`, `no_tokens` and `token_counter` resources from the ARC example. Actually defined on top of:
-[tokenizable.v](./theories/lib/tokenizable.v): More abstract version of above, does not constrain `token`s to only work for Fractionals.
-[Z_cmra.v](./theories/lib/Z_cmra.v): Instantiates the integers `Z` with addition as a cmra. The `≼` operation is trivial on these
-[int_as_nat_diff.v](./theories/lib/int_as_nat_diff.v): It is sometimes useful to represent `Z` as the difference between two (rising) natural numbers. This file extends the pure automation with such a concept. Used in `rwlock_linux_bounded` and the `inc_dec` counter.
-[loc_map.v](./theories/lib/loc_map.v): It is sometimes useful to be able to couple locations to specific data (often `gname`s). This file makes that doable without much hassle.
-[except_zero.v](./theories/lib/except_zero.v): Makes Diaframe strip off the except zero modality when possible when introducing hypotheses. Additionally, makes Diaframe strip off laters of Timeless hypotheses.
-[persistently.v](./theories/lib/persistently.v): Adds support for proving goals behind a `<pers>` modality.
-[intuitionistically.v](./theories/lib/intuitionistically.v): Adds support for proving goals behind a `□` modality.
-[iris_hints.v](./theories/lib/iris_hints.v): Adds hints specific to Iris's logic - rules for manipulating invariants.
-[own_hints.v](./theories/lib/own_hints.v): Adds hints for working with `own γ a` hypotheses, where `a` is a ghost element built from Iris's cmra building blocks (like `auth`, `agree`, `prod`, `option`, `excl`, etcetera.).
#### Files in [theories/heap_lang](./theories/heap_lang)
Contains all files relevant for instantiating the proof-search strategy for HeapLang
-`class_instances_heaplang.v`: registers the specifications of HeapLangs primitive operations to the proof search strategy.
-`biabd_instances_heaplang.v`: contains bi-abduction hints for the mapsto-resource, as well as some proof automation to deal with (in)equality of HeapLang values.
-`stepping_tacs.v`: bundles all required imports for the proof-search strategy instantiated for HeapLang, into one file.
#### Folders in `theories/examples`
-[class_instances_heaplang.v](./theories/heap_lang/class_instances_heaplang.v): registers the specifications of HeapLangs primitive operations to the proof search strategy.
-[biabd_instances_heaplang.v](./theories/heap_lang/biabd_instances_heaplang.v): contains bi-abduction hints for the mapsto-resource, as well as some proof automation to deal with (in)equality of HeapLang values.
-[stepping_tacs.v](./theories/heap_lang/stepping_tacs.v): bundles all required imports for the proof-search strategy instantiated for HeapLang, into one file.
#### Folders in [theories/examples](./theories/examples)
Contains 4 folders:
-`comparison`: Contains the 24 examples discussed in the paper.
-`external`: Contains subfolders with examples for lambda-rust, ReLoC, Actris and the iris-examples repository
-`sequential`: Showcases the proof-search strategy on some classical sequential algorithms
-`wip`: Contains various examples that are still work-in-progress.
#### Files in `theories/legacy`
-[comparison](./theories/examples/comparison): Contains the 24 examples discussed in the paper.
-[external](./theories/examples/external): Contains subfolders with examples for lambda-rust, ReLoC, Actris and the iris-examples repository
-[sequential](./theories/examples/sequential): Showcases the proof-search strategy on some classical sequential algorithms
-[wip](./theories/examples/wip): Contains various examples that are still work-in-progress.
#### Files in [theories/legacy](./theories/legacy)
