-
Notifications
You must be signed in to change notification settings - Fork 0
/
meta.yml
164 lines (124 loc) · 6.5 KB
/
meta.yml
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
---
# Usage: https://github.com/coq-community/templates#generating-configuration-files-using-the-generatesh-script
fullname: View-based semantics for hardware
shortname: view-hw
organization: kaist-cp
action: true
submodule: true
synopsis: View-based semantics for hardware
description: |-
This is the artifact for a paper, Kyeongmin Cho, Sung-Hwan Lee, Azalea Raad, and Jeehoon Kang,
"Revamping Hardware Persistency Models: View-Based and Axiomatic Persistency Models for Intel-x86
and Armv8", PLDI 2021.
This artifact provides mechanized proofs in the paper.
publications:
- pub_url: TBA
pub_title: Revamping Hardware Persistency Models (View-Based and Axiomatic Persistency Models for Intel-x86 and Armv8)
authors:
- name: Kyeongmin Cho
- name: Sung-Hwan Lee
- name: Azalea Raad
- name: Jeehoon Kang
maintainers:
- name: Kyeongmin Cho
opam-file-maintainer: [email protected]
opam-file-version: dev
license:
fullname: BSD 2-Clause
identifier: LICENSE
supported_coq_versions:
text: 8.13 or later
opam: '{ >= "8.13" }'
tested_coq_opam_versions:
- version: '8.13'
keywords:
- name: proof automation
build: |-
## Installation
We assume you are on **Ubuntu 20.04**.
### Requirements
- [opam](https://opam.ocaml.org/)
```
sudo apt install -y build-essential rsync opam
opam init
opam switch create 4.10.0 # or later. If your system OCaml version is >= 4.10.0, you can use it.
eval $(opam env)
opam update
```
- [Coq 8.13.1](https://coq.inria.fr/)
```
opam install coq.8.13.1
```
### Build
- `make -j quick`: quickly build without checking the proofs.
- `./build.sh`: build with checking all the proofs. It will incrementally copy the development to `.build` sub-directory, and then build there.
- `./status.sh`: check if there is any `admit` in the proofs. (It will print a single result, which is tactic in the library used for development and has nothing to do with the proofs.)
- Interactive Theorem Proving: use [ProofGeneral](https://proofgeneral.github.io/) or
[CoqIDE](https://coq.inria.fr/download). Note that `make` creates `_CoqProject`, which is then
used by ProofGeneral and CoqIDE. To use it:
+ ProofGeneral: use a recent version.
+ CoqIDE: configure it to use `_CoqProject`: `Edit` > `Preferences` > `Project`: change
`ignored` to `appended to arguments`.
categories:
- name: Computer Science/Equivalence proofs of semantics
documentation: |-
### Our results
Our proofs are based on [a prior work](https://github.com/snu-sf/promising-arm) for ARMv8-view, originally named "Promising-ARMv8". The prior work contains:
- the proof of the equivalence between ARMv8-view and ARMv8-axiom
- some proofs about certification
We extend the existing proofs for ARMv8 to persistency. In addition, we newly define Px86-view/Px86-axiom and prove the theorems of it mentioned in the paper.
#### Model
- `lib`(open source) and `src/lib` contain libraries not necessarily related to relaxed-memory concurrency and persistency.
- `src/lib/Lang.v`: Definition of assembly-like language and its interpretation for both x86 and ARMv8 (corresponding to Figure 13)
- `src/promising/TsoPromising.v`: Definition of Px86-view and Px86-prom (corresponding to Figure 11 and 12)
- `src/axiomatic/TsoAxiomatic.v`: Definition of Px86-axiom (corresponding to Figure 7)
- `src/promising/Promising.v`: Definition of PARMv8-view without
certification (corresponding to Figure 14, 15 and 16)
- `src/axiomatic/Axiomatic.v`: Definition of PARMv8-axiom (corresponding to Figure 9)
- `src/lcertify`: Thread-local certification
#### Results
- Theorem 5.3: Equivalence between Px86-view and Px86-axiom
+ Theorem `axiomatic_to_promising` in `src/equiv/TsoAtoP.v`:
Px86-axiom refines Px86-prom.
+ Theorem `promising_to_axiomatic` in `src/equiv/TsoPFtoA.v`:
Px86-prom refines Px86-axiom.
* `TsoPFtoA1.v`: construction of axiomatic execution from promising execution
* `TsoPFtoA2.v`, `TsoPFtoA3.v`: definitions and lemmas for main proof
* `TsoPFtoA4*.v`: proof for validity of constructed axiomatic execution
* `TsoPFtoA4SL.v`: simulation between promising and axiomatic execution
* `TsoPFtoA4OBR.v`, `TsoPFtoA4OBW.v`, `TsoPFtoA4FR.v`, `TsoPFtoA4FOB.v`, `TsoPFtoA4FP.v`: proof for "external" axiom
+ Lemma 5.1: Equivalence between Px86-prom and Px86-view
* The paper says that after the x86-prom and x86-view have been proven to be equivalent (Theorem 5.2)
and then extended to persistency, the proof in Coq was done right away.
* Theorem `promising_to_view` in `src/equiv/TsoPFtoV.v`:
Px86-prom refines Px86-view.
* Theorem `view_to_promising` in `src/equiv/TsoVtoP.v`:
Px86-view refines Px86-prom.
- Theorem 6.2: Equivalence between PARMv8-view and PARMv8-axiom
+ Theorem `axiomatic_to_promising` in `src/equiv/AtoP.v`:
PARMv8-axiom refines PARMv8-view without certification.
+ Theorem `promising_to_axiomatic` in `src/equiv/PFtoA.v`:
PARMv8-view without certification refines PARMv8-axiom.
* `PFtoA1.v`: construction of axiomatic execution from promising execution
* `PFtoA2.v`, `PFtoA3.v`: definitions and lemmas for main proof
* `PFtoA4*.v`: proof for validity of constructed axiomatic execution
* `PFtoA4SL.v`: simulation between promising and axiomatic execution
* `PFtoA4OBR.v`, `PFtoA4OBW.v`, `PFtoA4FR.v`, `PFtoA4FOB.v`, `PFtoA4FP.v`: proof for "external" axiom
* `PFtoA4Atomic.v`: proof for "atomic" axiom
+ Theorem `certified_exec_equivalent` in `src/lcertify/CertifyComplete.v`:
PARMv8-view and PARMv8-view without certification are equivalent.
### Results of prior work
Theorems included in the code but not directly related to what we did are:
- Theorem `certified_deadlock_free` in `src/lcertify/CertifyProgressRiscV.v`:
Promising-RISC-V is deadlock-free.
- Theorem `certified_promise_correct` in `src/lcertify/FindCertify.v`:
`find_and_certify` is correct.
+ Theorem `certified_promise_sound` in `src/lcertify/FindCertify.v`:
Assume the thread configuration `<T, M>` is certified, and promising
`p` leads to `<T', M'>`. Then `<T'. M'>` is certified if `p` is in
`find_and_certify <T, M>`.
+ Theorem `certified_promise_complete` in `src/lcertify/FindCertify.v`:
Assume the thread configuration `<T, M>` is certified, and promising
`p` leads to `<T', M'>`. Then `p` is in `find_and_certify <T, M>` if
`<T', M'>` is certified.
---