Added sample for snaphot #878
Conversation
Test/civl/samples/snapshot.bpl
Outdated
| yield procedure {:layer 0} read_r1({:linear} tid: One Tid) returns (r1_copy: [int]StampedValue); | ||
| refines action_read_r1; | ||
|
|
||
| atomic action {:layer 1} write ({:linear} tid: One Tid, v:Value, i: int) |
There was a problem hiding this comment.
Note that there is no yield procedure that calls write. This means that if you were to declare any yield invariants in this file, they would not be checked for interference against write.
Test/civl/samples/snapshot.bpl
Outdated
| } | ||
| } | ||
|
|
||
| yield procedure {:layer 0} read_s({:linear} tid: One Tid, i: int); |
There was a problem hiding this comment.
There is pattern in this file that is common in Civl programs. There is a single yield procedure that refines a particular atomic action (although it is allowed for many yield procedures to refine the same action). In such situations, I tend to follow a consistent way of declaring each such pair of a yield procedure and an action---write them together in a consistent order, either always procedure followed by action or the other way round.
Since this pattern is so common, it may be helpful for reducing syntactic clutter to provide each such pair with a single syntactic declaration such as the following:
yield procedure Foo(...) returns (...)
// other yield procedure specs here
refines left/right/both action
{
// action body here
}
{
// yield procedure body here
}
The syntax above would allow both the yield procedure and the action to share a single interface declaration.
There was a problem hiding this comment.
yes, this syntax makes sense. Has it been implemented?
There was a problem hiding this comment.
No, this syntax does not exist right now.
Test/civl/samples/snapshot.bpl
Outdated
| invariant {:layer 1} (forall j:int :: 1 <= j && j < i ==> r1[tid->val][j]->ts <= mem[j]->ts); | ||
| invariant {:layer 1} (forall j:int :: 1 <= j && j < i ==> (r1[tid->val][j]->ts == mem[j]->ts ==> r1[tid->val][j]->value == mem[j]->value)); | ||
| { | ||
| call read_f(tid, i); |
There was a problem hiding this comment.
read_f and read_s are abstractions of a single primitive read operations. It would be nice to write the sample in this manner.
- Define
readas a primitive yield procedure with the natural specification - Define
read_fandread_sas abstractions ofreadwith their current specifications.read_fwould be a yield procedure that callsreadand refines the atomic action you have already written.read_swould be similar.
There was a problem hiding this comment.
Will procedure read have no body, and will it refine an action that reads the value in memory and returns the value?
Test/civl/samples/snapshot.bpl
Outdated
| } | ||
| } | ||
|
|
||
| atomic action {:layer 2} write (v:Value, i: int) |
There was a problem hiding this comment.
Change the layer annotation of write to {:layer 1,3} to indicate that write co-exists with read, read_f, read_s, and scan'.
Change the layer annotation of action_read to {:layer 1,3} for the same reason. You could choose to rename write to action_write to capture the symmetry with action_read.
It is clear that action_read_f and action_read_s exist only at layer 2, which is as it should be.
There was a problem hiding this comment.
Also, it is nicer to move both read and write towards the bottom of the file so that layers are ordered bottom to top.
Test/civl/samples/snapshot.bpl
Outdated
| } | ||
| } | ||
|
|
||
| atomic action {:layer 2} write (v:Value, i: int) |
There was a problem hiding this comment.
Also, it is nicer to move both read and write towards the bottom of the file so that layers are ordered bottom to top.
Added a sample for the snapshot algorithm which returns an atomic snapshot using the double collect trick without using locks.