Skip to content
GitLab
Explore
Sign in
Primary navigation
Search or go to…
Project
Iris
Manage
Activity
Members
Labels
Plan
Issues
Issue boards
Milestones
Wiki
Code
Merge requests
Repository
Branches
Commits
Tags
Repository graph
Compare revisions
Build
Pipelines
Jobs
Pipeline schedules
Artifacts
Deploy
Releases
Package Registry
Model registry
Operate
Terraform modules
Monitor
Service Desk
Analyze
Value stream analytics
Contributor analytics
CI/CD analytics
Repository analytics
Model experiments
Help
Help
Support
GitLab documentation
Compare GitLab plans
Community forum
Contribute to GitLab
Provide feedback
Terms and privacy
Keyboard shortcuts
?
Snippets
Groups
Projects
Show more breadcrumbs
Pierre Roux
Iris
Commits
86a8269d
Verified
Commit
86a8269d
authored
5 years ago
by
Paolo G. Giarrusso
Browse files
Options
Downloads
Patches
Plain Diff
CAS -> CmpXchg in HeapLang tactic docs
parent
6aa60678
No related branches found
Branches containing commit
No related tags found
Tags containing commit
No related merge requests found
Changes
1
Hide whitespace changes
Inline
Side-by-side
Showing
1 changed file
docs/heap_lang.md
+4
-4
4 additions, 4 deletions
docs/heap_lang.md
with
4 additions
and
4 deletions
docs/heap_lang.md
+
4
−
4
View file @
86a8269d
...
...
@@ -7,7 +7,7 @@ language for simple examples.
## Language
HeapLang is a lambda-calculus with operations to allocate individual locations,
`load`
,
`store`
,
`C
AS
`
(compare-and-
swap
) and
`FAA`
(fetch-and-add). Moreover,
`load`
,
`store`
,
`C
mpXchg
`
(compare-and-
exchange
) and
`FAA`
(fetch-and-add). Moreover,
it has a
`fork`
construct to spawn new threads. In terms of values, we have
integers, booleans, unit, heap locations, as well as (binary) sums and products.
...
...
@@ -82,11 +82,11 @@ Tactics for the heap:
assertion in the spatial context, and fails if it cannot be found.
-
`wp_store`
: Reduce a store operation. This automatically finds the points-to
assertion in the spatial context, and fails if it cannot be found.
-
`wp_c
as
_suc`
,
`wp_c
as
_fail`
: Reduce a succeeding/failing C
AS
. This
-
`wp_c
mpxchg
_suc`
,
`wp_c
mpxchg
_fail`
: Reduce a succeeding/failing C
mpXchg
. This
automatically finds the points-to assertion. It also automatically tries to
solve the (in)equality to show that the C
AS
succeeds/fails, and opens a new
solve the (in)equality to show that the C
mpXchg
succeeds/fails, and opens a new
goal if it cannot prove this goal.
-
`wp_c
as
as H1 | H2`
: Reduce a C
AS
, performing a case distinction over whether
-
`wp_c
mpxchg
as H1 | H2`
: Reduce a C
mpXchg
, performing a case distinction over whether
it succeeds or fails. This automatically finds the points-to assertion. The
proof of equality in the first new subgoal will be called
`H1`
, and the proof
of the inequality in the second new subgoal will be called
`H2`
.
...
...
This diff is collapsed.
Click to expand it.
Preview
0%
Loading
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Save comment
Cancel
Please
register
or
sign in
to comment