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
3f6560fa
Commit
3f6560fa
authored
Nov 02, 2018
by
Daniel Gratzer
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Updated references
parent
53de53db
Changes
1
Hide whitespace changes
Inline
Sidebyside
Showing
1 changed file
with
16 additions
and
17 deletions
+16
17
README.md
README.md
+16
17
No files found.
README.md
View file @
3f6560fa
...
...
@@ 17,9 +17,8 @@ Iron has been built and tested with the following dependencies

In
[
theories/algebra
](
theories/algebra
)
two new cameras are defined.
1.
Improper fractions as a camera without identity with addition as
the operation are defined in
[
theories/algebra/vfrac.v
](
theories/algebra/vfrac.v
)
.
2.
The fractional authoritative camera described in Section 5 built
with improper fractions is defined in
[
theories/algebra/vfrac_auth.v
](
theories/algebra/vfrac_auth.v
)
.
2.
The fractional authoritative camera described in Section 6 with improper fractions is defined
in
[
theories/algebra/vfrac_auth.v
](
theories/algebra/vfrac_auth.v
)
.

The semantics of the connectives of fractional predicates logic are given in
[
theories/bi/fracpred.v
](
theories/bi/fracpred.v
)
.
...
...
@@ 33,29 +32,29 @@ Iron has been built and tested with the following dependencies
fractional predicates is contained in
[
theories/proofmode
](
theories/proofmode
)
.

In
[
theories/iron_logic
](
theories/iron_logic
)
much of the core Iron logic
discussed in Section
2
is defined.
discussed in Section
3
is defined.
*
_Uniformity_ with respect to fractions is defined in
[
theories/iron_logic/iron.v
](
theories/iron_logic/iron.v
)
as
`Uniform`
and
several closure properties of it are proved.
*
_Trackable invariants_ as discussed in Section
2.1
are formalized
*
_Trackable invariants_ as discussed in Section
3.2
are formalized
in
[
theories/iron_logic/fcinv.v
](
theories/iron_logic/fcinv.v
)
.
*
The definition of weakest preconditions from Section
4
is in
*
The definition of weakest preconditions from Section
6
is in
[
theories/iron_logic/weakestpre.v
](
theories/iron_logic/weakestpre.v
)
.

The formalization specific to the λref,conc is in
[
theories/heap_lang
](
theories/heap_lang
)
.
*
The definition of the heap in terms of ghost state from Section
5
is in
*
The definition of the heap in terms of ghost state from Section
6
is in
[
theories/heap_lang/heap.v
](
theories/heap_lang/heap.v
)
as
`heapG`
. So too
are the definitions of ↦ and 𝖊 (in the formalization called
`perm`
).
*
The theorems stated in Section
5
about updates to the heap ghost
*
The theorems stated in Section
6
about updates to the heap ghost
state are proven in
[
theories/heap_lang/heap.v
](
theories/heap_lang/heap.v
)
.
*
The state interpretation from Section
5
is defined in
*
The state interpretation from Section
6
is defined in
[
theories/heap_lang/heap.v
](
theories/heap_lang/heap.v
)
as
`heap_ctx`
.
*
Theorems
2
.1
, 2.2, 4.1,
and
4.2
are proven in
*
Theorems
3
.1 and
6.1
are proven in
[
theories/heap_lang/adequacy.v
](
theories/heap_lang/adequacy.v
)
.
*
The operational semantics from Figure
4
are defined in
*
The operational semantics from Figure
5
are defined in
[
theories/heap_lang/lang.v
](
theories/heap_lang/lang.v
)
.
*
The rules from Figures
1, 2, 3,
and
5
are proven in
*
The rules from Figures
4
and
7
are proven in
[
theories/heap_lang/lifting.v
](
theories/heap_lang/lifting.v
)
.

All of the examples of the paper are formalized and may be found in
...
...
@@ 67,11 +66,11 @@ Iron has been built and tested with the following dependencies
As mentioned in the paper, a small portion of
`par`
cannot be formalized in
the lifted logic but in the formalization this is factored out into
`spawn`
in
[
theories/heap_lang/lib/spawn.v
](
theories/heap_lang/lib/spawn.v
)
*
The example from
3
.1 is in
[
theories/heap_lang/lib/resource_transfer_par.v
](
theories/heap_lang/lib/resource_transfer_par.v
)
.
*
The example from
3
.2 is in
[
theories/heap_lang/lib/resource_transfer_fork.v
](
theories/heap_lang/lib/resource_transfer_fork.v
)
.
*
The example from
3
.3 is in
[
theories/heap_lang/lib/message_passing.v
](
theories/heap_lang/lib/message_passing.v
)
.
*
The example from
3
.4 is in
[
theories/heap_lang/lib/message_passing_example.v
](
theories/heap_lang/lib/message_passing_example.v
)
.
*
The example from
3
.5 is in
[
theories/heap_lang/lib/par.v
](
theories/heap_lang/lib/resource_transfer_par.v
)
.
*
The example from
4
.1 is in
[
theories/heap_lang/lib/resource_transfer_par.v
](
theories/heap_lang/lib/resource_transfer_par.v
)
.
*
The example from
4
.2 is in
[
theories/heap_lang/lib/resource_transfer_fork.v
](
theories/heap_lang/lib/resource_transfer_fork.v
)
.
*
The example from
4
.3 is in
[
theories/heap_lang/lib/message_passing.v
](
theories/heap_lang/lib/message_passing.v
)
.
*
The example from
4
.4 is in
[
theories/heap_lang/lib/message_passing_example.v
](
theories/heap_lang/lib/message_passing_example.v
)
.
*
The example from
4
.5 is in
[
theories/heap_lang/lib/par.v
](
theories/heap_lang/lib/resource_transfer_par.v
)
.
Note that
`spawn.v`
,
`resource_transfer_par.v`
, and
`resource_transfer_fork.v`
use the same state transition system (from Figure 3). This is formalized in
...
...
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