-
Notifications
You must be signed in to change notification settings - Fork 112
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
yes, this syntax makes sense. Has it been implemented?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
No, this syntax does not exist right now.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I have left comments regarding how to convert this sample into a test.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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
read
as a primitive yield procedure with the natural specification - Define
read_f
andread_s
as abstractions ofread
with their current specifications.read_f
would be a yield procedure that callsread
and refines the atomic action you have already written.read_s
would be similar.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Will procedure read
have no body, and will it refine an action that reads the value in memory and returns the value?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Yes
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The only manadatory feedback is to convert the sample into a test. Everything else is optional.
Test/civl/samples/snapshot.bpl
Outdated
} | ||
} | ||
|
||
atomic action {:layer 2} write (v:Value, i: int) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.