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
Tutorial POPL18
Commits
843053be
Commit
843053be
authored
Feb 01, 2019
by
Ralf Jung
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
avoid mapping '.' path
parent
2d2cb7bc
Pipeline
#14339
failed with stage
in 6 minutes and 37 seconds
Changes
6
Pipelines
1
Show whitespace changes
Inline
Side-by-side
Showing
6 changed files
with
7 additions
and
5 deletions
+7
-5
.gitignore
.gitignore
+1
-0
_CoqProject
_CoqProject
+2
-1
exercises/ex_04_parallel_add.v
exercises/ex_04_parallel_add.v
+1
-1
exercises/ex_05_parallel_add_mul.v
exercises/ex_05_parallel_add_mul.v
+1
-1
solutions/ex_04_parallel_add.v
solutions/ex_04_parallel_add.v
+1
-1
solutions/ex_05_parallel_add_mul.v
solutions/ex_05_parallel_add_mul.v
+1
-1
No files found.
.gitignore
View file @
843053be
...
...
@@ -30,3 +30,4 @@ Makefile.coq*
*.crashcoqide
.coqdeps.d
build-dep
_opam
_CoqProject
View file @
843053be
-Q . tutorial
-Q exercises exercises
-Q solutions solutions
-arg -w -arg -notation-overridden,-redundant-canonical-projection,-several-object-files
exercises/ex_01_swap.v
exercises/ex_02_sumlist.v
...
...
exercises/ex_04_parallel_add.v
View file @
843053be
...
...
@@ -6,7 +6,7 @@ threads increase a reference that's initially zero by two, the result is four.
From
iris
.
algebra
Require
Import
auth
frac_auth
.
From
iris
.
base_logic
.
lib
Require
Import
invariants
.
From
iris
.
heap_lang
Require
Import
lib
.
par
proofmode
notation
.
From
tutorial
Require
Import
ex_03_spinlock
.
From
exercises
Require
Import
ex_03_spinlock
.
(** The program as a heap-lang expression. We use the heap-lang [par] module for
parallel composition. *)
...
...
exercises/ex_05_parallel_add_mul.v
View file @
843053be
...
...
@@ -11,7 +11,7 @@ Contrary to the earlier exercises, this exercise is nearly entirely open.
From
iris
.
algebra
Require
Import
auth
frac_auth
.
From
iris
.
base_logic
.
lib
Require
Import
invariants
.
From
iris
.
heap_lang
Require
Import
proofmode
notation
lib
.
par
.
From
tutorial
Require
Import
ex_03_spinlock
.
From
exercises
Require
Import
ex_03_spinlock
.
Definition
parallel_add_mul
:
expr
:
=
let
:
"r"
:
=
ref
#
0
in
...
...
solutions/ex_04_parallel_add.v
View file @
843053be
...
...
@@ -6,7 +6,7 @@ threads increase a reference that's initially zero by two, the result is four.
From
iris
.
algebra
Require
Import
auth
frac_auth
.
From
iris
.
base_logic
.
lib
Require
Import
invariants
.
From
iris
.
heap_lang
Require
Import
lib
.
par
proofmode
notation
.
From
tutorial
Require
Import
ex_03_spinlock
.
From
solutions
Require
Import
ex_03_spinlock
.
(** The program as a heap-lang expression. We use the heap-lang [par] module for
parallel composition. *)
...
...
solutions/ex_05_parallel_add_mul.v
View file @
843053be
...
...
@@ -11,7 +11,7 @@ Contrary to the earlier exercises, this exercise is nearly entirely open.
From
iris
.
algebra
Require
Import
auth
frac_auth
.
From
iris
.
base_logic
.
lib
Require
Import
invariants
.
From
iris
.
heap_lang
Require
Import
proofmode
notation
lib
.
par
.
From
tutorial
Require
Import
ex_03_spinlock
.
From
solutions
Require
Import
ex_03_spinlock
.
Definition
parallel_add_mul
:
expr
:
=
let
:
"r"
:
=
ref
#
0
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