Skip to content
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.

Sign up for GitHub

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

Jump to bottom

Added sample for snaphot #878

Merged
merged 4 commits into from
Apr 28, 2024
Merged

Added sample for snaphot #878

Changes from 1 commit
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
f5c7a8a
Added sample for snaphot
NamrathaG Apr 26, 2024
ab86f48
fixed order of proc and action
NamrathaG Apr 26, 2024
b5b7b86
updated reads to return
NamrathaG Apr 26, 2024
4d08980
layer fixes
NamrathaG Apr 27, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
116 changes: 116 additions & 0 deletions Test/civl/samples/snapshot.bpl
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,116 @@
type Value;
shazqadeer marked this conversation as resolved.
Show resolved Hide resolved

type Tid;

datatype StampedValue {
StampedValue(ts: int, value: Value)
}

var {:layer 0,2} mem: [int]StampedValue;
var {:layer 0,1} r1: [Tid][int]StampedValue;
var {:layer 0,1} r2: [Tid][int]StampedValue;

const n: int;
axiom n >= 1;

atomic action {:layer 2} scan'({:linear} tid: One Tid) returns (snapshot: [int]StampedValue)
{
assume (forall j:int :: 1 <= j && j <= n ==> snapshot[j] == mem[j]);
}

yield procedure {:layer 1} scan({:linear} tid: One Tid) returns (snapshot: [int]StampedValue)
refines scan';
{
var i: int;
var b: bool;

while (true)
invariant {:yields} {:layer 1} true;
{
i := 1;
while (i <= n)
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);
Copy link
Contributor

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 and read_s as abstractions of read with their current specifications. read_f would be a yield procedure that calls read and refines the atomic action you have already written. read_s would be similar.

Copy link
Collaborator Author

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?

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes

i := i + 1;
}

i := 1;
while (i <= n)
invariant {:layer 1} (forall j:int :: 1 <= j && j < i ==> mem[j]->ts <= r2[tid->val][j]->ts);
invariant {:layer 1} (forall j:int :: 1 <= j && j < i ==> (r2[tid->val][j]->ts == mem[j]->ts ==> r2[tid->val][j]->value == mem[j]->value));
{
call read_s(tid, i);
i := i + 1;
}

assert {:layer 1} (forall j:int :: 1 <= j && j <= n ==> (r1[tid->val][j] == r2[tid->val][j] ==> r1[tid->val][j] == mem[j]));

call b := equality_check(tid);
if (b) {
assert {:layer 1} (forall j:int :: 1 <= j && j <= n ==> r1[tid->val][j] == mem[j]);
call snapshot := read_r1(tid);
break;
}
}
}

both action {:layer 1} action_equality_check({:linear} tid: One Tid) returns (b: bool)
{
b := (forall j:int :: 1 <= j && j <= n ==> r1[tid->val][j] == r2[tid->val][j]);
}

yield procedure {:layer 0} equality_check({:linear} tid: One Tid) returns (b: bool);
refines action_equality_check;

both action {:layer 1} action_read_r1({:linear} tid: One Tid) returns (r1_copy: [int]StampedValue)
{
r1_copy := r1[tid->val];
}

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)
Copy link
Contributor

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.

modifies mem;
{
var x: StampedValue;
x := mem[i];
mem[i] := StampedValue(x->ts + 1, v);
}

yield procedure {:layer 0} read_f ({:linear} tid: One Tid, i: int);
refines action_read_f;

right action {:layer 1} action_read_f ({:linear} tid: One Tid, i: int)
modifies r1;
{
var {:pool "K"} k:int;
var {:pool "V"} v:Value;
if (*) {
assume {:add_to_pool "K", mem[i]->ts, k} {:add_to_pool "V", mem[i]->value, v} true;
assume k < mem[i]->ts;
r1[tid->val][i] := StampedValue(k, v);
} else {
r1[tid->val][i] := mem[i];
}
}

yield procedure {:layer 0} read_s({:linear} tid: One Tid, i: int);
Copy link
Contributor

@shazqadeer shazqadeer Apr 26, 2024 •
edited
Loading

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.

Copy link
Collaborator Author

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?

Copy link
Contributor

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.

refines action_read_s;

left action {:layer 1} action_read_s({:linear} tid: One Tid, i: int)
modifies r2;
{
var {:pool "K"} k:int;
var {:pool "V"} v:Value;

if (*) {
assume {:add_to_pool "K", mem[i]->ts, k} {:add_to_pool "V", mem[i]->value, v} true;
assume k > mem[i]->ts;
r2[tid->val][i] := StampedValue(k, v);
} else {
r2[tid->val][i] := mem[i];
}
}
Loading