Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
What's new
10
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Open sidebar
Iris
Iron
Commits
53de53db
Commit
53de53db
authored
Nov 02, 2018
by
Aleš Bizjak
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Make the README correspond to the updated paper.
parent
3027b51a
Pipeline
#12632
passed with stage
in 6 minutes and 7 seconds
Changes
1
Pipelines
1
Hide whitespace changes
Inline
Side-by-side
Showing
1 changed file
with
69 additions
and
69 deletions
+69
-69
README.md
README.md
+69
-69
No files found.
README.md
View file @
53de53db
# Iron: Managing Obligations in Higher-Order Concurrent Separation Logic
This repository contains the Iron logic, as described in the POPL'19 paper
"Iron: Managing Obligations in Higher-Order Concurrent Separation Logic" by
"
[
Iron: Managing Obligations in Higher-Order Concurrent Separation Logic
](
https://iris-project.org/pdfs/2018-iron.pdf
)
" by
Aleš Bizjak, Daniel Gratzer, Robbert Krebbers, and Lars Birkedal.
## Building Iron
...
...
@@ -163,71 +163,71 @@ are also defined using the fancy update modality. They may be found in
## A Correspondence of Theorems, Definitions, and Examples in the Paper to the Formalization
While the correspondence between the contents of the paper and the
formalization
is discussed above, we
have
provide
d
an explicit table
for convenience.
The format of the table is as follows: Name of
The
orem/Rule/Definition/Proposition, the name in the formalization,
and the file in the formalization.
-
The language definition in Section 2,
`expr`
,
`theories/heap_lang/lang
.v`
-
`
e`
and
`↦`
,
`perm`
and
`↦`
,
`theories/heap_lang/heap
.v`
-
Trackable invariants,
`fcinv`
,
`
theories/
i
ro
n
_logic/
fcinv
.v`
-
`
OPerm(-, -)`
,
`fcinv_own`
,
`
theories/
i
ro
n
_logic/
fcinv
.v`
-
`
DPerm(-, -)`
,
`fcinv_cancel_own`
,
`theories/iron_logic/fc
in
v
.v`
-
`HOARE-
FRAME`
,
`hoare_frame_r`
,
`iris-coq/theories/program_logic/hoare.v`
-
`
HOARE-VAL`
,
`ht_val`
,
`iris-coq/theories/program_logic/hoare
.v`
-
`
HOARE-λ`
,
`pure_rec`
,
`
theories/heap_lang/
lifting
.v`
-
`
HOARE-BIND`
,
`ht_bind`
,
`iris-coq/theories/program_logic/hoare
.v`
-
`
EMP-SPLIT`
,
`perm_split`
,
`
theories/heap_lang/
heap
.v`
-
`
PT-SPLIT`
,
`mapsto_uniform`
,
`
theories/heap_lang/
heap
.v`
-
`
PT-DISJ`
,
`mapsto_valid_2`
,
`
theories/heap_lang/
heap
.v`
-
`HOARE-
ALLOC`
,
`wp_alloc`
,
`
theories/heap_lang/lifting.v`
-
`HOARE-F
REE`
,
`wp_free`
,
`
theories/heap_lang/lifting.v`
-
`
HOARE-LOAD`
,
`wp_load`
,
`
theories/heap_lang/lifting.v`
-
`
HOARE-STORE`
,
`wp_store`
,
`theories/heap_lang/lifting
.v`
-
`
HOARE-FORK-EMP`
/
`HOARE-FORK-TRUE`
,
`wp_fork`
,
`theories/heap_lang/lifting
.v`
-
`INV-
DUP`
,
`inv_persistent`
,
`theories/heap_lang/lift
in
g
.v`
-
`INV-
ALLOC`
,
`inv_alloc`
,
`iris-coq
/theories/
base
_logic/
lib/invariants
.v`
-
`INV-
OPEN`
,
`inv_open`
,
`iris-coq
/theories/
base
_logic/
lib/invariants
.v`
-
`TINV-
SPLIT`
,
`fcinv_o
wn_fractional`
,
`
theories/iron_logic/fcinv.v`
-
`TINV-D
UP`
,
`fcinv_persistent`
,
`
theories/iron_logic/fcinv.v`
-
`TINV-ALLOC`
,
`fcinv_alloc_named`
,
`
theories/iron_logic/
fcinv
.v`
-
`
TINV-OPEN`
,
`fcinv_open`
,
`
theories/
i
ro
n
_logic/
fcinv
.v`
-
`TINV-DEALLOC`
,
`fcinv_cancel`
,
`theories/iron_logic/fcinv
.v`
-
Unif
orm
with respect to fractions,
`Uniform`
,
`theories/iron_logic/iron
.v`
-
`HOARE-CONS`
,
`ht_vs`
,
`iris-coq/theories/program_logic/hoare
.v`
-
The rules from Figure 4,
`head_step`
,
`
theories/heap_lang/l
ang
.v`
-
The
ore
m
2
.1
,
`heap_adequacy`
,
`theories/heap_lang/adequacy
.v`
-
The
orem 2.2,
`heap_strong_adequacy`
,
`theories/heap_lang/adequacy
.v`
-
`HOARE-PAR`
,
`par_spec`
,
`
theories/heap_lang/lib/
par
.v`
-
The example from
3.1,
`transfer_works1`
,
`
theories/heap_lang/lib/
r
es
ource_tranfer_par
.v`
-
The
example from 3.2,
`transfer_works1`
,
`
theories/heap_lang/lib/
resource_tranfer_fork
.v`
-
The example from
3.3, Several theorems,
`
theories/heap_lang/lib/message_passing.v`
-
The example from
3.4,
`program_spec`
,
`theories/heap_lang/lib/message_passing_example
.v`
-
The example from 3.5, Several theorems,
`theories/heap_lang/lib/{spawn, par}
.v`
-
Definition
s
of lifted
connectives, Several definitions,
`theories/bi/fracpred
.v`
-
Definition of lifted
`↦`
,
`↦`
,
`theories/heap_lang/heap
.v`
-
`LHOARE-
FRAME`
,
`iron_wp_
frame_r`
,
`iris-coq/theories/program_logic/hoare.v`
-
`LHOARE-
VAL`
,
`iron_wp_val`
,
`iris-coq/theories/program_logic/hoare
.v`
-
`LHOARE-
λ`
,
`pure_rec`
,
`theories/heap_lang/lifting
.v`
-
`L
HOARE-BIND`
,
`iron_wp_bind`
,
`iris-coq/theories/program_logic/hoare
.v`
-
`L
PT-DISJ`
,
`mapsto_valid_2`
,
`
theories/heap_lang/
heap
.v`
-
`LHOARE-
ALLOC`
,
`iron_wp_
alloc`
,
`
theories/heap_lang/lifting.v`
-
`LHOARE-
FREE`
,
`iron_wp_
free`
,
`
theories/heap_lang/lifting.v`
-
`LHOARE-
LOAD`
,
`iron_wp_
load`
,
`
theories/heap_lang/lifting.v`
-
`LHOARE-
STORE`
,
`iron_wp_
store`
,
`
theories/heap_lang/lifting.v`
-
`L
HOARE-FORK`
,
`iron_wp_fork`
,
`theories/heap_lang/lift
in
g
.v`
-
`LTINV-
SPLIT`
,
`fcinv_
own_fractional`
,
`
theories/iron_logic/fcinv.v`
-
`LTINV-
DUP`
,
`fcinv_persistent`
,
`
theories/iron_logic/fcinv.v`
-
`LTINV-
ALLOC`
,
`fcinv_
alloc_named`
,
`
theories/iron_logic/fcinv.v`
-
`LTINV-
OPEN`
,
`fcinv_open`
,
`
theories/iron_logic/fcinv.v`
-
`LTINV-DEALLOC`
,
`fcinv_cancel`
,
`
theories/iron_logic/
fcinv
.v`
-
Definition of Hoare triples,
`iron_wp`
,
`theories/iron_logic/weakestpre
.v`
-
Theorem
4.1,
`heap_adequacy`
,
`
theories/heap_lang/adequacy.v`
-
Theorem 4.2,
`heap_strong_adequacy`
,
`theories/heap_lang/adequacy
.v`
-
Definition of
WP in Section 5,
`wp_def`
,
`iris-coq/theories/program_logic/weakestpre
.v`
-
Definition of state interp from Section 5,
`heap_ctx`
,
`theories/heap_lang/heap
.v`
-
The
orem 5.1,
`wp_strong_all_adequacy`
,
`iris-coq/theories/program_logic/adequ
ac
y
.v`
While the correspondence between the contents of the paper and the
formalization
is discussed above, we
also
provide an explicit table
for convenience.
| Paper definition or theorem | Coq definition or theorem | File |
|-------|--------|---------|
|
The
language definition in Sec. 3 |
`expr`
|
`iron/theories/heap_lang/lang.v`
|
|
`𝖊`
and
`↪`
|
`perm`
and
`↦`
|
`iron/theories/heap_lang/heap.v`
|
| Trackable invariants |
`fcinv`
|
`iron/theories/iron_logic/fcinv.v`
|
|
`OPerm(-, -)`
|
`fcinv_own`
|
`iron/theories/iron_logic/fcinv
.v`
|
|
`
DPerm(-, -)`
|
`fcinv_cancel_own`
|
`iron/theories/iron_logic/fcinv
.v`
|
|
`HOARE-FRAME`
|
`hoare_frame_r`
|
`iris-coq/
theories/
p
ro
gram
_logic/
hoare
.v`
|
|
`
HOARE-VAL`
|
`ht_val`
|
`iris-coq/
theories/
p
ro
gram
_logic/
hoare
.v`
|
|
`
HOARE-λ`
|
`pure_rec`
|
`iron/theories/heap_lang/lift
in
g
.v`
|
|
`HOARE-
BIND`
|
`ht_bind`
|
`iris-coq/theories/program_logic/hoare.v`
|
|
`
EMP-SPLIT`
|
`perm_split`
|
`iron/theories/heap_lang/heap
.v`
|
|
`
PT-SPLIT`
|
`mapsto_uniform`
|
`iron/
theories/heap_lang/
heap
.v`
|
|
`
PT-DISJ`
|
`mapsto_valid_2`
|
`iron/theories/heap_lang/heap
.v`
|
|
`
HOARE-ALLOC`
|
`wp_alloc`
|
`iron/
theories/heap_lang/
lifting
.v`
|
|
`
HOARE-FREE`
|
`wp_free`
|
`iron/
theories/heap_lang/
lifting
.v`
|
|
`
HOARE-LOAD`
|
`wp_load`
|
`iron/
theories/heap_lang/
lifting
.v`
|
|
`HOARE-
STORE`
|
`wp_store`
|
`iron/
theories/heap_lang/lifting.v`
|
|
`HOARE-F
ORK-EMP`
/
`HOARE-FORK-TRUE`
|
`wp_fork`
|
`iron/
theories/heap_lang/lifting.v`
|
|
`
INV-DUP`
|
`inv_persistent`
|
`iron/
theories/heap_lang/lifting.v`
|
|
`
INV-ALLOC`
|
`inv_alloc`
|
`iris-coq/theories/base_logic/lib/invariants
.v`
|
|
`
INV-OPEN`
|
`inv_open`
|
`iris-coq/theories/base_logic/lib/invariants
.v`
|
|
`
T
INV-
SPLIT`
|
`fcinv_own_fractional`
|
`iron/theories/iron_logic/fc
in
v
.v`
|
|
`
T
INV-
DUP`
|
`fcinv_persistent`
|
`iron
/theories/
iron
_logic/
fcinv
.v`
|
|
`
T
INV-
ALLOC`
|
`fcinv_alloc_named`
|
`iron
/theories/
iron
_logic/
fcinv
.v`
|
|
`TINV-
OPEN`
|
`fcinv_o
pen`
|
`iron/
theories/iron_logic/fcinv.v`
|
|
`TINV-D
EALLOC`
|
`fcinv_cancel`
|
`iron/
theories/iron_logic/fcinv.v`
|
| Uniform with respect to fractions |
`Uniform`
|
`iron/
theories/iron_logic/
iron
.v`
|
|
`
HOARE-CONS`
|
`ht_vs`
|
`iris-coq/
theories/
p
ro
gram
_logic/
hoare
.v`
|
| The rules from Figure 5 |
`head_step`
|
`iron/theories/heap_lang/lang
.v`
|
| The
or
e
m
3.1 |
`heap_basic_adequacy`
|
`iron/theories/heap_lang/adequacy
.v`
|
| Theorem 3.2 |
`heap_all_adequacy`
|
`iron/theories/heap_lang/adequacy
.v`
|
|
`HOARE-PAR`
|
`par_spec`
|
`iron/
theories/heap_lang/l
ib/par
.v`
|
|
The
example fro
m
4
.1
|
`transfer_works1`
|
`iron/theories/heap_lang/lib/resource_transfer_par
.v`
|
|
The
rules from Figure 6 | Several theorems |
`iron/theories/heap_lang/lib/resource_transfer_sts
.v`
|
| The example from 4.2 |
`transfer_works1`
|
`iron/
theories/heap_lang/lib/
resource_transfer_fork
.v`
|
|
The example from
4.3 | Several theorems |
`iron/
theories/heap_lang/lib/
m
es
sage_passing
.v`
|
|
The
queue specifications from 4.3 | Several theorems in Section
`queue_bag_spec`
|
`iron/
theories/heap_lang/lib/
queue
.v`
|
|
The example from
4.4 |
`program_spec`
|
`iron/
theories/heap_lang/lib/message_passing
_example
.v`
|
|
The example from
4.5 | Several theorems |
`iron/theories/heap_lang/lib/{spawn,par}
.v`
|
| Definitions of lifted connectives | Several definitions |
`iron/theories/bi/fracpred
.v`
|
|
Definition of lifted
`↦`
|
`↦`
|
`iron/theories/heap_lang/heap
.v`
|
|
`LHOARE-FRAME`
|
`iron_wp_frame_r`
|
`iris-coq/theories/program_logic/hoare
.v`
|
|
`LHOARE-
VAL`
|
`iron_wp_
val`
|
`iris-coq/theories/program_logic/hoare.v`
|
|
`LHOARE-
λ`
|
`pure_rec`
|
`iron/theories/heap_lang/lifting
.v`
|
|
`LHOARE-
BIND`
|
`iron_wp_bind`
|
`iris-coq/theories/program_logic/hoare
.v`
|
|
`L
PT-DISJ`
|
`mapsto_valid_2`
|
`iron/theories/heap_lang/heap
.v`
|
|
`L
HOARE-ALLOC`
|
`iron_wp_alloc`
|
`iron/
theories/heap_lang/
lifting
.v`
|
|
`LHOARE-
FREE`
|
`iron_wp_
free`
|
`iron/
theories/heap_lang/lifting.v`
|
|
`LHOARE-
LOAD`
|
`iron_wp_
load`
|
`iron/
theories/heap_lang/lifting.v`
|
|
`LHOARE-
STORE`
|
`iron_wp_
store`
|
`iron/
theories/heap_lang/lifting.v`
|
|
`LHOARE-
FORK`
|
`iron_wp_
fork`
|
`iron/
theories/heap_lang/lifting.v`
|
|
`L
TINV-SPLIT`
|
`fcinv_own_fractional`
|
`iron/theories/iron_logic/fc
in
v
.v`
|
|
`LTINV-
DUP`
|
`fcinv_
persistent`
|
`iron/
theories/iron_logic/fcinv.v`
|
|
`LTINV-
ALLOC`
|
`fcinv_alloc_named`
|
`iron/
theories/iron_logic/fcinv.v`
|
|
`LTINV-
OPEN`
|
`fcinv_
open`
|
`iron/
theories/iron_logic/fcinv.v`
|
|
`LTINV-
DEALLOC`
|
`fcinv_cancel`
|
`iron/
theories/iron_logic/fcinv.v`
|
| Definition of Hoare triples |
`iron_wp`
|
`iron/
theories/iron_logic/
weakestpre
.v`
|
| Theorem 5.1 |
`heap_basic_adequacy`
|
`iron/theories/heap_lang/adequacy
.v`
|
|
Theorem
5.2 |
`heap_
all_
adequacy`
|
`iron/
theories/heap_lang/adequacy.v`
|
| Definition of WP in Section 6 |
`wp_def`
|
`iris-coq/theories/program_logic/weakestpre
.v`
|
|
Definition of
state interpretation from Section 6 |
`heap_ctx`
|
`iron/theories/heap_lang/heap
.v`
|
| Theorem 6.1 |
`wp_strong_all_adequacy`
|
`iris-coq/theories/program_logic/adequacy
.v`
|
|
The
lock specifications | Several theorems |
`iron/theories/heap_lang/lib/spin_lock_tr
ac
k
.v`
|
| Adequacy for the lock |
`lock_always_freed`
|
`iron/theories/heap_lang/lib/spin_lock_track.v`
|
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment