Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Dan Frumin
ReLoC-v1
Commits
928a1c39
Commit
928a1c39
authored
Jul 06, 2016
by
Robbert Krebbers
Browse files
Merge branch 'master' of bitbucket.org:logsem/iris-logrel
parents
efe1b574
e378869b
Changes
19
Hide whitespace changes
Inline
Side-by-side
F_mu_ref_
par
/context_refinement.v
→
F_mu_ref_
conc
/context_refinement.v
View file @
928a1c39
From
iris_logrel
.
F_mu_ref_
par
Require
Export
fundamental_binary
.
From
iris_logrel
.
F_mu_ref_
conc
Require
Export
fundamental_binary
.
Inductive
ctx_item
:=
|
CTX_Rec
...
...
F_mu_ref_
par
/examples/counter.v
→
F_mu_ref_
conc
/examples/counter.v
View file @
928a1c39
From
iris
.
proofmode
Require
Import
invariants
ghost_ownership
tactics
.
From
iris_logrel
.
F_mu_ref_
par
Require
Export
examples
.
lock
.
From
iris_logrel
.
F_mu_ref_
par
Require
Import
soundness_binary
.
From
iris_logrel
.
F_mu_ref_
conc
Require
Export
examples
.
lock
.
From
iris_logrel
.
F_mu_ref_
conc
Require
Import
soundness_binary
.
Definition
CG_increment
(
x
:
expr
)
:
expr
:=
Rec
(
Store
x
.[
ren
(
+
2
)]
(
BinOp
Add
(
♯
1
)
(
Load
x
.[
ren
(
+
2
)]))).
...
...
F_mu_ref_
par
/examples/lock.v
→
F_mu_ref_
conc
/examples/lock.v
View file @
928a1c39
From
iris
.
proofmode
Require
Import
invariants
ghost_ownership
tactics
.
From
iris_logrel
.
F_mu_ref_
par
Require
Export
rules_binary
typing
.
From
iris_logrel
.
F_mu_ref_
conc
Require
Export
rules_binary
typing
.
Definition
newlock
:
expr
:=
Alloc
(
♭
false
).
Definition
acquire
:
expr
:=
...
...
F_mu_ref_
par
/examples/stack/CG_stack.v
→
F_mu_ref_
conc
/examples/stack/CG_stack.v
View file @
928a1c39
From
iris
.
proofmode
Require
Import
invariants
ghost_ownership
tactics
.
From
iris_logrel
.
F_mu_ref_
par
Require
Import
examples
.
lock
.
From
iris_logrel
.
F_mu_ref_
conc
Require
Import
examples
.
lock
.
Import
uPred
.
Definition
CG_StackType
τ
:=
...
...
F_mu_ref_
par
/examples/stack/FG_stack.v
→
F_mu_ref_
conc
/examples/stack/FG_stack.v
View file @
928a1c39
From
iris_logrel
.
F_mu_ref_
par
Require
Import
typing
.
From
iris_logrel
.
F_mu_ref_
conc
Require
Import
typing
.
Definition
FG_StackType
τ
:=
TRec
(
Tref
(
TSum
TUnit
(
TProd
τ
.[
ren
(
+
1
)]
(
TVar
0
)))).
...
...
F_mu_ref_
par
/examples/stack/refinement.v
→
F_mu_ref_
conc
/examples/stack/refinement.v
View file @
928a1c39
From
iris
.
program_logic
Require
Import
auth
.
From
iris_logrel
.
F_mu_ref_
par
Require
Import
soundness_binary
.
From
iris_logrel
.
F_mu_ref_
par
.
examples
Require
Import
lock
.
From
iris_logrel
.
F_mu_ref_
par
.
examples
.
stack
Require
Import
From
iris_logrel
.
F_mu_ref_
conc
Require
Import
soundness_binary
.
From
iris_logrel
.
F_mu_ref_
conc
.
examples
Require
Import
lock
.
From
iris_logrel
.
F_mu_ref_
conc
.
examples
.
stack
Require
Import
CG_stack
FG_stack
stack_rules
.
From
iris
.
proofmode
Require
Import
invariants
ghost_ownership
tactics
.
...
...
F_mu_ref_
par
/examples/stack/stack_rules.v
→
F_mu_ref_
conc
/examples/stack/stack_rules.v
View file @
928a1c39
From
iris
.
proofmode
Require
Import
invariants
ghost_ownership
tactics
.
From
iris_logrel
.
F_mu_ref_
par
Require
Import
logrel_binary
.
From
iris_logrel
.
F_mu_ref_
conc
Require
Import
logrel_binary
.
From
iris
.
algebra
Require
Import
gmap
dec_agree
.
From
iris
.
program_logic
Require
Import
auth
.
Import
uPred
.
...
...
F_mu_ref_
par
/fundamental_binary.v
→
F_mu_ref_
conc
/fundamental_binary.v
View file @
928a1c39
From
iris_logrel
.
F_mu_ref_
par
Require
Export
logrel_binary
.
From
iris_logrel
.
F_mu_ref_
conc
Require
Export
logrel_binary
.
From
iris
.
proofmode
Require
Import
tactics
pviewshifts
invariants
.
From
iris_logrel
.
F_mu_ref_
par
Require
Import
rules_binary
.
From
iris_logrel
.
F_mu_ref_
conc
Require
Import
rules_binary
.
From
iris
.
algebra
Require
Export
upred_big_op
.
Section
bin_log_def
.
...
...
F_mu_ref_
par
/fundamental_unary.v
→
F_mu_ref_
conc
/fundamental_unary.v
View file @
928a1c39
From
iris_logrel
.
F_mu_ref_
par
Require
Export
logrel_unary
.
From
iris_logrel
.
F_mu_ref_
par
Require
Import
rules
.
From
iris_logrel
.
F_mu_ref_
conc
Require
Export
logrel_unary
.
From
iris_logrel
.
F_mu_ref_
conc
Require
Import
rules
.
From
iris
.
algebra
Require
Export
upred_big_op
.
From
iris
.
proofmode
Require
Import
tactics
pviewshifts
invariants
.
...
...
F_mu_ref_
par
/lang.v
→
F_mu_ref_
conc
/lang.v
View file @
928a1c39
File moved
F_mu_ref_
par
/logrel_binary.v
→
F_mu_ref_
conc
/logrel_binary.v
View file @
928a1c39
From
iris
.
proofmode
Require
Import
tactics
.
From
iris
.
program_logic
Require
Export
weakestpre
.
From
iris_logrel
.
F_mu_ref_
par
Require
Export
rules_binary
typing
.
From
iris_logrel
.
F_mu_ref_
conc
Require
Export
rules_binary
typing
.
Import
uPred
.
(
*
HACK
:
move
somewhere
else
*
)
...
...
F_mu_ref_
par
/logrel_unary.v
→
F_mu_ref_
conc
/logrel_unary.v
View file @
928a1c39
From
iris
.
proofmode
Require
Import
tactics
.
From
iris
.
program_logic
Require
Export
weakestpre
.
From
iris_logrel
.
F_mu_ref_
par
Require
Export
rules
typing
.
From
iris_logrel
.
F_mu_ref_
conc
Require
Export
rules
typing
.
Import
uPred
.
Definition
logN
:
namespace
:=
nroot
.
@
"logN"
.
...
...
F_mu_ref_
par
/rules.v
→
F_mu_ref_
conc
/rules.v
View file @
928a1c39
...
...
@@ -3,7 +3,7 @@ From iris.program_logic Require Export weakestpre global_functor invariants.
From
iris
.
program_logic
Require
Import
lifting
.
From
iris
.
algebra
Require
Import
upred_big_op
frac
dec_agree
.
From
iris
.
program_logic
Require
Import
ownership
auth
.
From
iris_logrel
.
F_mu_ref_
par
Require
Export
lang
.
From
iris_logrel
.
F_mu_ref_
conc
Require
Export
lang
.
Import
uPred
.
Definition
heapN
:
namespace
:=
nroot
.
@
"heap"
.
...
...
F_mu_ref_
par
/rules_binary.v
→
F_mu_ref_
conc
/rules_binary.v
View file @
928a1c39
From
iris
.
program_logic
Require
Import
lifting
.
From
iris
.
algebra
Require
Import
upred_big_op
frac
dec_agree
.
From
iris
.
program_logic
Require
Import
ownership
auth
.
From
iris_logrel
.
F_mu_ref_
par
Require
Export
rules
.
From
iris_logrel
.
F_mu_ref_
conc
Require
Export
rules
.
From
iris
.
proofmode
Require
Import
tactics
weakestpre
invariants
.
Import
uPred
.
...
...
F_mu_ref_
par
/soundness_binary.v
→
F_mu_ref_
conc
/soundness_binary.v
View file @
928a1c39
From
iris_logrel
.
F_mu_ref_
par
Require
Export
context_refinement
.
From
iris_logrel
.
F_mu_ref_
conc
Require
Export
context_refinement
.
From
iris
.
algebra
Require
Import
upred_big_op
frac
dec_agree
.
From
iris
.
program_logic
Require
Import
ownership
auth
.
From
iris
.
proofmode
Require
Import
tactics
pviewshifts
invariants
.
...
...
F_mu_ref_
par
/soundness_unary.v
→
F_mu_ref_
conc
/soundness_unary.v
View file @
928a1c39
From
iris_logrel
.
F_mu_ref_
par
Require
Export
fundamental_unary
.
From
iris_logrel
.
F_mu_ref_
conc
Require
Export
fundamental_unary
.
From
iris
.
proofmode
Require
Import
tactics
pviewshifts
.
From
iris
.
program_logic
Require
Import
ownership
adequacy
auth
.
...
...
F_mu_ref_
par
/typing.v
→
F_mu_ref_
conc
/typing.v
View file @
928a1c39
From
iris_logrel
.
F_mu_ref_
par
Require
Export
lang
.
From
iris_logrel
.
F_mu_ref_
conc
Require
Export
lang
.
Inductive
type
:=
|
TUnit
:
type
...
...
_CoqProject
View file @
928a1c39
...
...
@@ -18,20 +18,20 @@ F_mu_ref/rules.v
F_mu_ref/logrel.v
F_mu_ref/fundamental.v
F_mu_ref/soundness.v
F_mu_ref_par/lang.v
F_mu_ref_par/rules.v
F_mu_ref_par/typing.v
F_mu_ref_par/logrel_unary.v
F_mu_ref_par/fundamental_unary.v
F_mu_ref_par/rules_binary.v
F_mu_ref_par/logrel_binary.v
F_mu_ref_par/fundamental_binary.v
F_mu_ref_par/soundness_unary.v
F_mu_ref_par/context_refinement.v
F_mu_ref_par/soundness_binary.v
F_mu_ref_par/examples/lock.v
F_mu_ref_par/examples/counter.v
F_mu_ref_par/examples/stack/stack_rules.v
F_mu_ref_par/examples/stack/CG_stack.v
F_mu_ref_par/examples/stack/FG_stack.v
F_mu_ref_par/examples/stack/refinement.v
\ No newline at end of file
F_mu_ref_conc/lang.v
F_mu_ref_conc/rules.v
F_mu_ref_conc/typing.v
F_mu_ref_conc/logrel_unary.v
F_mu_ref_conc/fundamental_unary.v
F_mu_ref_conc/rules_binary.v
F_mu_ref_conc/logrel_binary.v
F_mu_ref_conc/fundamental_binary.v
F_mu_ref_conc/soundness_unary.v
F_mu_ref_conc/context_refinement.v
F_mu_ref_conc/soundness_binary.v
F_mu_ref_conc/examples/lock.v
F_mu_ref_conc/examples/counter.v
F_mu_ref_conc/examples/stack/stack_rules.v
F_mu_ref_conc/examples/stack/CG_stack.v
F_mu_ref_conc/examples/stack/FG_stack.v
F_mu_ref_conc/examples/stack/refinement.v
\ No newline at end of file
prelude/base.v
View file @
928a1c39
...
...
@@ -45,4 +45,4 @@ Ltac solve_proper_alt :=
Reserved
Notation
"⟦ τ ⟧"
(
at
level
0
,
τ
at
level
70
).
Reserved
Notation
"⟦ τ ⟧ₑ"
(
at
level
0
,
τ
at
level
70
).
Reserved
Notation
"⟦ Γ ⟧*"
(
at
level
0
,
Γ
at
level
70
).
\ No newline at end of file
Reserved
Notation
"⟦ Γ ⟧*"
(
at
level
0
,
Γ
at
level
70
).
Write
Preview
Supports
Markdown
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