зеркало из https://github.com/microsoft/ivy.git
removing tabs from MSV examples
This commit is contained in:
Kenneth McMillan
Родитель
08a581a019
Коммит
b6ff8f1e26
|
|
@ -13,10 +13,7 @@ Project("{8BC9CEB8-8B4A-11D0-8D11-00A0C91BC942}") = "hello4", "hello4.vcxproj",
|
|||
EndProject
|
||||
Global
|
||||
GlobalSection(SolutionConfigurationPlatforms) = preSolution
|
||||
Debug|x64 = Debug|x64
|
||||
Debug|x86 = Debug|x86
|
||||
Release|x64 = Release|x64
|
||||
Release|x86 = Release|x86
|
||||
EndGlobalSection
|
||||
GlobalSection(ProjectConfigurationPlatforms) = postSolution
|
||||
{5D1E04F7-4717-4DC2-976E-0F5CD418F4D3}.Debug|x64.ActiveCfg = Debug|x64
|
||||
|
|
|
|||
|
|
@ -34,14 +34,14 @@ object spec = {
|
|||
# This says to initialize `pending` to `false`.
|
||||
|
||||
after init {
|
||||
pending := false
|
||||
pending := false
|
||||
}
|
||||
|
||||
# This says, before executing the implementation of `hello`, set
|
||||
# `pending` to true.
|
||||
|
||||
before hello(val:t) {
|
||||
pending := true
|
||||
pending := true
|
||||
}
|
||||
|
||||
# This says, before executing the implementation of `world`,
|
||||
|
|
@ -49,8 +49,8 @@ object spec = {
|
|||
# an unsolicited call to `world`, this assertion will fail.
|
||||
|
||||
before world(val:t) {
|
||||
assert pending;
|
||||
pending := false
|
||||
assert pending;
|
||||
pending := false
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -59,7 +59,7 @@ object spec = {
|
|||
|
||||
object impl = {
|
||||
implement hello {
|
||||
call world(val+1)
|
||||
call world(val+1)
|
||||
}
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -28,18 +28,18 @@ object spec = {
|
|||
var hello_value : t
|
||||
|
||||
after init {
|
||||
pending := false
|
||||
pending := false
|
||||
}
|
||||
|
||||
before hello(val:t) {
|
||||
pending := true;
|
||||
hello_value := val # remember the value
|
||||
pending := true;
|
||||
hello_value := val # remember the value
|
||||
}
|
||||
|
||||
before world(val:t) {
|
||||
assert pending;
|
||||
assert val > hello_value; # new assertion
|
||||
pending := false
|
||||
assert pending;
|
||||
assert val > hello_value; # new assertion
|
||||
pending := false
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -47,7 +47,7 @@ object spec = {
|
|||
|
||||
object impl = {
|
||||
implement hello {
|
||||
call world(val+1)
|
||||
call world(val+1)
|
||||
}
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -27,19 +27,19 @@ object spec = {
|
|||
var hello_value : t
|
||||
|
||||
after init {
|
||||
pending := false
|
||||
pending := false
|
||||
}
|
||||
|
||||
before hello(val:t) {
|
||||
assert val + 1 ~= 0; # val is not max
|
||||
pending := true;
|
||||
hello_value := val
|
||||
assert val + 1 ~= 0; # val is not max
|
||||
pending := true;
|
||||
hello_value := val
|
||||
}
|
||||
|
||||
before world(val:t) {
|
||||
assert pending;
|
||||
assert val > hello_value;
|
||||
pending := false
|
||||
assert pending;
|
||||
assert val > hello_value;
|
||||
pending := false
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -52,7 +52,7 @@ object spec = {
|
|||
|
||||
object impl = {
|
||||
implement hello {
|
||||
call world(val+1)
|
||||
call world(val+1)
|
||||
}
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -26,21 +26,21 @@ object spec = {
|
|||
var side : side_t
|
||||
|
||||
after init {
|
||||
side := left
|
||||
side := left
|
||||
}
|
||||
|
||||
# When `ping` occurs, the ball must be on the left. It moves to the right.
|
||||
|
||||
before intf.ping {
|
||||
assert side = left;
|
||||
side := right
|
||||
assert side = left;
|
||||
side := right
|
||||
}
|
||||
|
||||
# When `pong` occurs, the ball must be on the rightr. It moves to the left.
|
||||
|
||||
before intf.pong {
|
||||
assert side = right;
|
||||
side := left
|
||||
assert side = right;
|
||||
side := left
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -55,14 +55,14 @@ object left_player = {
|
|||
init ball
|
||||
|
||||
action hit = {
|
||||
if ball {
|
||||
call intf.ping;
|
||||
ball := false
|
||||
}
|
||||
if ball {
|
||||
call intf.ping;
|
||||
ball := false
|
||||
}
|
||||
}
|
||||
|
||||
implement intf.pong {
|
||||
ball := true
|
||||
ball := true
|
||||
}
|
||||
|
||||
}
|
||||
|
|
@ -75,14 +75,14 @@ object right_player = {
|
|||
init ~ball
|
||||
|
||||
action hit = {
|
||||
if ball {
|
||||
call intf.pong;
|
||||
ball := false
|
||||
}
|
||||
if ball {
|
||||
call intf.pong;
|
||||
ball := false
|
||||
}
|
||||
}
|
||||
|
||||
implement intf.ping {
|
||||
ball := true
|
||||
ball := true
|
||||
}
|
||||
|
||||
}
|
||||
|
|
|
|||
|
|
@ -11,10 +11,7 @@ Project("{8BC9CEB8-8B4A-11D0-8D11-00A0C91BC942}") = "pingpong_bad", "pingpong_ba
|
|||
EndProject
|
||||
Global
|
||||
GlobalSection(SolutionConfigurationPlatforms) = preSolution
|
||||
Debug|x64 = Debug|x64
|
||||
Debug|x86 = Debug|x86
|
||||
Release|x64 = Release|x64
|
||||
Release|x86 = Release|x86
|
||||
EndGlobalSection
|
||||
GlobalSection(ProjectConfigurationPlatforms) = postSolution
|
||||
{A48A9407-CA01-4B56-8D51-303F4FC5F6E1}.Debug|x64.ActiveCfg = Debug|x64
|
||||
|
|
|
|||
|
|
@ -12,13 +12,13 @@ object spec = {
|
|||
init side = left
|
||||
|
||||
before intf.ping {
|
||||
assert side = left;
|
||||
side := right
|
||||
assert side = left;
|
||||
side := right
|
||||
}
|
||||
|
||||
before intf.pong {
|
||||
assert side = right;
|
||||
side := left
|
||||
assert side = right;
|
||||
side := left
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -27,12 +27,12 @@ object left_player = {
|
|||
init ball
|
||||
|
||||
action hit = {
|
||||
call intf.ping; # forgot to test ball!
|
||||
ball := false
|
||||
call intf.ping; # forgot to test ball!
|
||||
ball := false
|
||||
}
|
||||
|
||||
implement intf.pong {
|
||||
ball := true
|
||||
ball := true
|
||||
}
|
||||
|
||||
conjecture left_player.ball -> spec.side = left
|
||||
|
|
@ -43,14 +43,14 @@ object right_player = {
|
|||
init ~ball
|
||||
|
||||
action hit = {
|
||||
if ball {
|
||||
call intf.pong;
|
||||
ball := false
|
||||
}
|
||||
if ball {
|
||||
call intf.pong;
|
||||
ball := false
|
||||
}
|
||||
}
|
||||
|
||||
implement intf.ping {
|
||||
ball := true
|
||||
ball := true
|
||||
}
|
||||
|
||||
conjecture right_player.ball -> spec.side = right
|
||||
|
|
|
|||
|
|
@ -22,19 +22,19 @@ object spec = {
|
|||
var side : side_t
|
||||
|
||||
after init {
|
||||
side := left
|
||||
side := left
|
||||
}
|
||||
|
||||
before intf.ping {
|
||||
assert side = left & ...;
|
||||
side := right
|
||||
assert side = left & ...;
|
||||
side := right
|
||||
}
|
||||
|
||||
# When `pong` occurs, the ball must be on the rightr. It moves to the left.
|
||||
|
||||
before intf.pong {
|
||||
assert side = right & ...;
|
||||
side := left
|
||||
assert side = right & ...;
|
||||
side := left
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -47,15 +47,15 @@ object left_player = {
|
|||
...
|
||||
|
||||
action hit = {
|
||||
if ball {
|
||||
call intf.ping(...);
|
||||
ball := false
|
||||
}
|
||||
if ball {
|
||||
call intf.ping(...);
|
||||
ball := false
|
||||
}
|
||||
}
|
||||
|
||||
implement intf.pong(val:t) {
|
||||
ball := true;
|
||||
...
|
||||
ball := true;
|
||||
...
|
||||
}
|
||||
|
||||
}
|
||||
|
|
@ -67,15 +67,15 @@ object right_player = {
|
|||
...
|
||||
|
||||
action hit = {
|
||||
if ball {
|
||||
call intf.pong(...);
|
||||
ball := false
|
||||
}
|
||||
if ball {
|
||||
call intf.pong(...);
|
||||
ball := false
|
||||
}
|
||||
}
|
||||
|
||||
implement intf.ping(val:t) {
|
||||
ball := true;
|
||||
...
|
||||
ball := true;
|
||||
...
|
||||
}
|
||||
|
||||
}
|
||||
|
|
|
|||
|
|
@ -9,10 +9,7 @@ Project("{8BC9CEB8-8B4A-11D0-8D11-00A0C91BC942}") = "pingpong_ex_right", "pingpo
|
|||
EndProject
|
||||
Global
|
||||
GlobalSection(SolutionConfigurationPlatforms) = preSolution
|
||||
Debug|x64 = Debug|x64
|
||||
Debug|x86 = Debug|x86
|
||||
Release|x64 = Release|x64
|
||||
Release|x86 = Release|x86
|
||||
EndGlobalSection
|
||||
GlobalSection(ProjectConfigurationPlatforms) = postSolution
|
||||
{A48A9407-CA01-4B56-8D51-303F4FC5F6E1}.Debug|x64.ActiveCfg = Debug|x64
|
||||
|
|
|
|||
|
|
@ -22,19 +22,19 @@ object spec = {
|
|||
var side : side_t
|
||||
|
||||
after init {
|
||||
side := left
|
||||
side := left
|
||||
}
|
||||
|
||||
before intf.ping {
|
||||
assert side = left & (val/2)*2 = val;
|
||||
side := right
|
||||
assert side = left & (val/2)*2 = val;
|
||||
side := right
|
||||
}
|
||||
|
||||
# When `pong` occurs, the ball must be on the rightr. It moves to the left.
|
||||
|
||||
before intf.pong {
|
||||
assert side = right & (val/2)*2+1 = val;
|
||||
side := left
|
||||
assert side = right & (val/2)*2+1 = val;
|
||||
side := left
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -46,19 +46,19 @@ object left_player = {
|
|||
init ball
|
||||
var next : t
|
||||
after init {
|
||||
next := 0;
|
||||
next := 0;
|
||||
}
|
||||
|
||||
action hit = {
|
||||
if ball {
|
||||
call intf.ping(next);
|
||||
ball := false
|
||||
}
|
||||
if ball {
|
||||
call intf.ping(next);
|
||||
ball := false
|
||||
}
|
||||
}
|
||||
|
||||
implement intf.pong(val:t) {
|
||||
ball := true;
|
||||
next := val + 1;
|
||||
ball := true;
|
||||
next := val + 1;
|
||||
}
|
||||
|
||||
}
|
||||
|
|
@ -70,15 +70,15 @@ object right_player = {
|
|||
var next : t
|
||||
|
||||
action hit = {
|
||||
if ball {
|
||||
call intf.pong(next);
|
||||
ball := false
|
||||
}
|
||||
if ball {
|
||||
call intf.pong(next);
|
||||
ball := false
|
||||
}
|
||||
}
|
||||
|
||||
implement intf.ping(val:t) {
|
||||
ball := true;
|
||||
next := val + 1;
|
||||
ball := true;
|
||||
next := val + 1;
|
||||
}
|
||||
|
||||
}
|
||||
|
|
|
|||
|
|
@ -13,19 +13,19 @@ module message_queue(net_msg,seq_num) = {
|
|||
instance imap : ordered_map_impl(seq_num,net_msg.t)
|
||||
|
||||
implement enqueue {
|
||||
call imap.set(net_msg.num(msg),msg)
|
||||
call imap.set(net_msg.num(msg),msg)
|
||||
}
|
||||
|
||||
implement empty {
|
||||
res := seq_num.iter.is_end(imap.lub(seq_num.iter.create(0)))
|
||||
res := seq_num.iter.is_end(imap.lub(seq_num.iter.create(0)))
|
||||
}
|
||||
|
||||
implement delete_all(seq:seq_num.t) {
|
||||
call imap.erase(seq_num.iter.create(0),seq_num.iter.create(seq_num.next(seq)))
|
||||
call imap.erase(seq_num.iter.create(0),seq_num.iter.create(seq_num.next(seq)))
|
||||
}
|
||||
|
||||
implement pick_one {
|
||||
res := imap.get(seq_num.iter.val(imap.lub(seq_num.iter.create(0))),res)
|
||||
res := imap.get(seq_num.iter.val(imap.lub(seq_num.iter.create(0))),res)
|
||||
}
|
||||
|
||||
}
|
||||
|
|
|
|||
|
|
@ -60,9 +60,9 @@ type request_kind = {write,read}
|
|||
|
||||
object request_body = {
|
||||
type t = struct {
|
||||
knd : request_kind,
|
||||
ky : key,
|
||||
vl : value
|
||||
knd : request_kind,
|
||||
ky : key,
|
||||
vl : value
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -72,8 +72,8 @@ object request_body = {
|
|||
|
||||
object request = {
|
||||
type t = struct {
|
||||
tx : txid,
|
||||
bd : request_body.t
|
||||
tx : txid,
|
||||
bd : request_body.t
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -83,7 +83,7 @@ object request = {
|
|||
|
||||
object response_body = {
|
||||
type t = struct {
|
||||
vl : value
|
||||
vl : value
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -92,8 +92,8 @@ object response_body = {
|
|||
|
||||
object response = {
|
||||
type t = struct {
|
||||
tx : txid,
|
||||
bd : response_body.t
|
||||
tx : txid,
|
||||
bd : response_body.t
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -107,15 +107,15 @@ object response = {
|
|||
module replica = {
|
||||
function store(K:key) : value
|
||||
after init {
|
||||
store(K) := 0
|
||||
store(K) := 0
|
||||
}
|
||||
action exec(inp : request_body.t) returns (out:response_body.t) = {
|
||||
if inp.knd = write {
|
||||
store(inp.ky) := inp.vl;
|
||||
}
|
||||
else if inp.knd = read {
|
||||
out.vl := store(inp.ky);
|
||||
}
|
||||
if inp.knd = write {
|
||||
store(inp.ky) := inp.vl;
|
||||
}
|
||||
else if inp.knd = read {
|
||||
out.vl := store(inp.ky);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -164,17 +164,17 @@ object ref = {
|
|||
relation committed(X:txid)
|
||||
|
||||
after init {
|
||||
next := 0;
|
||||
committed(X) := false;
|
||||
next := 0;
|
||||
committed(X) := false;
|
||||
}
|
||||
|
||||
# The create action simply generates a new transaction id and stores
|
||||
# the request.
|
||||
|
||||
implement create {
|
||||
tx := next;
|
||||
txs(tx) := inp;
|
||||
next := next + 1;
|
||||
tx := next;
|
||||
txs(tx) := inp;
|
||||
next := next + 1;
|
||||
}
|
||||
|
||||
# The commit action asserts that the transaction id must be for an
|
||||
|
|
@ -184,10 +184,10 @@ object ref = {
|
|||
# that the assertions are guarantees for the caller.
|
||||
|
||||
implement commit {
|
||||
assert 0 <= tx & tx < next;
|
||||
assert ~committed(tx);
|
||||
txres(tx) := rep.exec(txs(tx));
|
||||
committed(tx) := true;
|
||||
assert 0 <= tx & tx < next;
|
||||
assert ~committed(tx);
|
||||
txres(tx) := rep.exec(txs(tx));
|
||||
committed(tx) := true;
|
||||
}
|
||||
delegate commit
|
||||
|
||||
|
|
@ -195,8 +195,8 @@ object ref = {
|
|||
# be committed, then returns the stored result.
|
||||
|
||||
implement eval {
|
||||
assert committed(tx);
|
||||
res := txres(tx);
|
||||
assert committed(tx);
|
||||
res := txres(tx);
|
||||
}
|
||||
delegate eval
|
||||
|
||||
|
|
@ -250,11 +250,11 @@ module client(cid,srvr_chan,cl_chans) = {
|
|||
# server.
|
||||
|
||||
implement client_request {
|
||||
var m : req_msg;
|
||||
m.cid := cid;
|
||||
m.req.tx := ref.create(req,dst);
|
||||
m.req.bd := req;
|
||||
call srvr_chan.send(m);
|
||||
var m : req_msg;
|
||||
m.cid := cid;
|
||||
m.req.tx := ref.create(req,dst);
|
||||
m.req.bd := req;
|
||||
call srvr_chan.send(m);
|
||||
}
|
||||
|
||||
# To handle a response from the server, we simply pass it to the
|
||||
|
|
@ -262,7 +262,7 @@ module client(cid,srvr_chan,cl_chans) = {
|
|||
# "ghost" and is only used for specification.
|
||||
|
||||
implement cl_chans.recv(resp : response.t) {
|
||||
call client_response(resp.bd,resp.tx)
|
||||
call client_response(resp.bd,resp.tx)
|
||||
}
|
||||
|
||||
}
|
||||
|
|
@ -276,7 +276,7 @@ module server_node(port, cl_chans) = {
|
|||
instance rep : replica
|
||||
|
||||
instance req_chan : nondup_endpoint(port,req_msg)
|
||||
|
||||
|
||||
# When we receive a request message on our port, we first commit the
|
||||
# transaction id, then build a response message by executing the
|
||||
# trasnaction on the replica, then send the response to the client. In
|
||||
|
|
@ -289,12 +289,12 @@ module server_node(port, cl_chans) = {
|
|||
# verification.
|
||||
|
||||
implement req_chan.recv(inp : req_msg) {
|
||||
call ref.commit(inp.req.tx,dest.srvr);
|
||||
var rr := inp.req.bd;
|
||||
var res : response.t;
|
||||
res.tx := inp.req.tx;
|
||||
res.bd := rep.exec(rr);
|
||||
call cl_chans(inp.cid).send(res)
|
||||
call ref.commit(inp.req.tx,dest.srvr);
|
||||
var rr := inp.req.bd;
|
||||
var res : response.t;
|
||||
res.tx := inp.req.tx;
|
||||
res.bd := rep.exec(rr);
|
||||
call cl_chans(inp.cid).send(res)
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -334,13 +334,13 @@ object service_spec = {
|
|||
relation responded(X:txid)
|
||||
|
||||
after init {
|
||||
responded(X) := false;
|
||||
responded(X) := false;
|
||||
}
|
||||
|
||||
before cl_chans.send(p : client_id, m : response.t) {
|
||||
assert ~responded(m.tx);
|
||||
assert m.bd = ref.eval(m.tx);
|
||||
responded(m.tx) := true;
|
||||
assert ~responded(m.tx);
|
||||
assert m.bd = ref.eval(m.tx);
|
||||
responded(m.tx) := true;
|
||||
}
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -7,10 +7,7 @@ Project("{8BC9CEB8-8B4A-11D0-8D11-00A0C91BC942}") = "repstore1_srvr", "repstore1
|
|||
EndProject
|
||||
Global
|
||||
GlobalSection(SolutionConfigurationPlatforms) = preSolution
|
||||
Debug|x64 = Debug|x64
|
||||
Debug|x86 = Debug|x86
|
||||
Release|x64 = Release|x64
|
||||
Release|x86 = Release|x86
|
||||
EndGlobalSection
|
||||
GlobalSection(ProjectConfigurationPlatforms) = postSolution
|
||||
{A48A9407-CA01-4B56-8D51-303F4FC5F6E1}.Debug|x64.ActiveCfg = Debug|x64
|
||||
|
|
|
|||
|
|
@ -68,29 +68,29 @@ type request_kind = {write,read}
|
|||
|
||||
object request_body = {
|
||||
type t = struct {
|
||||
knd : request_kind,
|
||||
ky : key,
|
||||
vl : value
|
||||
knd : request_kind,
|
||||
ky : key,
|
||||
vl : value
|
||||
}
|
||||
}
|
||||
|
||||
object request = {
|
||||
type t = struct {
|
||||
tx : txid,
|
||||
bd : request_body.t
|
||||
tx : txid,
|
||||
bd : request_body.t
|
||||
}
|
||||
}
|
||||
|
||||
object response_body = {
|
||||
type t = struct {
|
||||
vl : value
|
||||
vl : value
|
||||
}
|
||||
}
|
||||
|
||||
object response = {
|
||||
type t = struct {
|
||||
tx : txid,
|
||||
bd : response_body.t
|
||||
tx : txid,
|
||||
bd : response_body.t
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -99,15 +99,15 @@ object response = {
|
|||
module replica = {
|
||||
function store(K:key) : value
|
||||
after init {
|
||||
store(K) := 0
|
||||
store(K) := 0
|
||||
}
|
||||
action exec(inp : request_body.t) returns (out:response_body.t) = {
|
||||
if inp.knd = write {
|
||||
store(inp.ky) := inp.vl;
|
||||
}
|
||||
else if inp.knd = read {
|
||||
out.vl := store(inp.ky);
|
||||
}
|
||||
if inp.knd = write {
|
||||
store(inp.ky) := inp.vl;
|
||||
}
|
||||
else if inp.knd = read {
|
||||
out.vl := store(inp.ky);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -137,27 +137,27 @@ object ref = {
|
|||
relation committed(X:txid)
|
||||
|
||||
after init {
|
||||
next := 0;
|
||||
committed(X) := false;
|
||||
next := 0;
|
||||
committed(X) := false;
|
||||
}
|
||||
|
||||
implement create {
|
||||
tx := next;
|
||||
txs(tx) := inp;
|
||||
next := next + 1;
|
||||
tx := next;
|
||||
txs(tx) := inp;
|
||||
next := next + 1;
|
||||
}
|
||||
|
||||
implement commit {
|
||||
assert 0 <= tx & tx < next;
|
||||
assert ~committed(tx);
|
||||
txres(tx) := rep.exec(txs(tx));
|
||||
committed(tx) := true;
|
||||
assert 0 <= tx & tx < next;
|
||||
assert ~committed(tx);
|
||||
txres(tx) := rep.exec(txs(tx));
|
||||
committed(tx) := true;
|
||||
}
|
||||
delegate commit
|
||||
|
||||
implement eval {
|
||||
assert committed(tx);
|
||||
res := txres(tx);
|
||||
assert committed(tx);
|
||||
res := txres(tx);
|
||||
}
|
||||
delegate eval
|
||||
|
||||
|
|
@ -181,7 +181,7 @@ object ser = {
|
|||
relation serialized(X:txid)
|
||||
|
||||
after init {
|
||||
serialized(X) := false;
|
||||
serialized(X) := false;
|
||||
}
|
||||
|
||||
# The serializer also keeps track of the order serialization in a
|
||||
|
|
@ -194,11 +194,11 @@ object ser = {
|
|||
# only serialize write transactions.
|
||||
|
||||
implement serialize {
|
||||
assert 0 <= tx & tx < ref.next;
|
||||
assert ~serialized(tx);
|
||||
assert ref.txs(tx).knd = write;
|
||||
serialized(tx) := true;
|
||||
call queue.push(tx);
|
||||
assert 0 <= tx & tx < ref.next;
|
||||
assert ~serialized(tx);
|
||||
assert ref.txs(tx).knd = write;
|
||||
serialized(tx) := true;
|
||||
call queue.push(tx);
|
||||
}
|
||||
delegate serialize
|
||||
|
||||
|
|
@ -206,9 +206,9 @@ object ser = {
|
|||
# in the order in which they are serialized.
|
||||
|
||||
before ref.commit(tx : txid,dst:dest.t) {
|
||||
if ref.txs(tx).knd = write {
|
||||
assert tx = queue.pop
|
||||
}
|
||||
if ref.txs(tx).knd = write {
|
||||
assert tx = queue.pop
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -244,15 +244,15 @@ module client(cid,prim_chan,sec_chan,cl_chans) = {
|
|||
# parameter `the_dst`.
|
||||
|
||||
implement client_request {
|
||||
var m : req_msg;
|
||||
m.cid := cid;
|
||||
m.req.tx := ref.create(req,the_dst);
|
||||
m.req.bd := req;
|
||||
if the_dst = dest.prim {
|
||||
call prim_chan.send(m);
|
||||
} else {
|
||||
call sec_chan.send(m);
|
||||
}
|
||||
var m : req_msg;
|
||||
m.cid := cid;
|
||||
m.req.tx := ref.create(req,the_dst);
|
||||
m.req.bd := req;
|
||||
if the_dst = dest.prim {
|
||||
call prim_chan.send(m);
|
||||
} else {
|
||||
call sec_chan.send(m);
|
||||
}
|
||||
}
|
||||
|
||||
# To handle a response from the server, we simply pass it to the
|
||||
|
|
@ -260,7 +260,7 @@ module client(cid,prim_chan,sec_chan,cl_chans) = {
|
|||
# "ghost" and is only used for specification.
|
||||
|
||||
implement cl_chans.recv(resp : response.t) {
|
||||
call client_response(resp.bd,resp.tx)
|
||||
call client_response(resp.bd,resp.tx)
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -284,9 +284,9 @@ module primary_node(port, fwd_chan, rev_chan, cl_chans) = {
|
|||
# Initially, all the counters are zero.
|
||||
|
||||
after init {
|
||||
pending(K) := 0;
|
||||
pending(K) := 0;
|
||||
}
|
||||
|
||||
|
||||
# When receiving a request message from a client, the primary
|
||||
# node must first check whether it is a read or a write. In the case
|
||||
# of a read, we check if the key has a pending write. If not, we commit
|
||||
|
|
@ -297,33 +297,33 @@ module primary_node(port, fwd_chan, rev_chan, cl_chans) = {
|
|||
#
|
||||
|
||||
implement req_chan.recv(inp : req_msg) {
|
||||
var rr := inp.req.bd;
|
||||
var rr := inp.req.bd;
|
||||
if rr.knd = read {
|
||||
if pending(rr.ky) = 0 {
|
||||
call ref.commit(inp.req.tx,dest.prim);
|
||||
var res : response.t;
|
||||
res.tx := inp.req.tx;
|
||||
res.bd := rep.exec(rr);
|
||||
call cl_chans(inp.cid).send(res)
|
||||
} else {
|
||||
if pending(rr.ky) = 0 {
|
||||
call ref.commit(inp.req.tx,dest.prim);
|
||||
var res : response.t;
|
||||
res.tx := inp.req.tx;
|
||||
res.bd := rep.exec(rr);
|
||||
call cl_chans(inp.cid).send(res)
|
||||
} else {
|
||||
call req_chan.send(inp); # if cannot execute, recirculate
|
||||
}
|
||||
} else if rr.knd = write {
|
||||
call ser.serialize(inp.req.tx); # this is ghost!
|
||||
call fwd_chan.send(inp);
|
||||
pending(rr.ky) := pending(rr.ky).next;
|
||||
var res := rep.exec(inp.req.bd);
|
||||
}
|
||||
}
|
||||
} else if rr.knd = write {
|
||||
call ser.serialize(inp.req.tx); # this is ghost!
|
||||
call fwd_chan.send(inp);
|
||||
pending(rr.ky) := pending(rr.ky).next;
|
||||
var res := rep.exec(inp.req.bd);
|
||||
}
|
||||
}
|
||||
|
||||
# When we receive a write request on the acknowledgement channel,
|
||||
# we decrement the pending count of the key.
|
||||
|
||||
implement rev_chan.recv(inp : req_msg) {
|
||||
var rr := inp.req.bd;
|
||||
if rr.knd = write {
|
||||
pending(rr.ky) := pending(rr.ky).prev;
|
||||
}
|
||||
var rr := inp.req.bd;
|
||||
if rr.knd = write {
|
||||
pending(rr.ky) := pending(rr.ky).prev;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -337,17 +337,17 @@ module secondary_node(port, fwd_chan, rev_chan, cl_chans) = {
|
|||
instance rep : replica
|
||||
|
||||
instance req_chan : nondup_endpoint(port,req_msg)
|
||||
|
||||
|
||||
implement req_chan.recv(inp : req_msg) {
|
||||
var rr := inp.req.bd;
|
||||
var rr := inp.req.bd;
|
||||
if rr.knd = read {
|
||||
var res : response.t;
|
||||
res.tx := inp.req.tx;
|
||||
res.bd := rep.exec(rr);
|
||||
call ref.commit(inp.req.tx,dest.sec);
|
||||
call cl_chans(inp.cid).send(res);
|
||||
}
|
||||
# ignore writes!
|
||||
var res : response.t;
|
||||
res.tx := inp.req.tx;
|
||||
res.bd := rep.exec(rr);
|
||||
call ref.commit(inp.req.tx,dest.sec);
|
||||
call cl_chans(inp.cid).send(res);
|
||||
}
|
||||
# ignore writes!
|
||||
}
|
||||
|
||||
# When the secondary receives a forwarded write from the primary,
|
||||
|
|
@ -356,12 +356,12 @@ module secondary_node(port, fwd_chan, rev_chan, cl_chans) = {
|
|||
#
|
||||
|
||||
implement fwd_chan.recv(inp : req_msg) {
|
||||
var res : response.t;
|
||||
res.tx := inp.req.tx;
|
||||
res.bd := rep.exec(inp.req.bd);
|
||||
call ref.commit(inp.req.tx,dest.sec);
|
||||
call cl_chans(inp.cid).send(res);
|
||||
call rev_chan.send(inp);
|
||||
var res : response.t;
|
||||
res.tx := inp.req.tx;
|
||||
res.bd := rep.exec(inp.req.bd);
|
||||
call ref.commit(inp.req.tx,dest.sec);
|
||||
call cl_chans(inp.cid).send(res);
|
||||
call rev_chan.send(inp);
|
||||
}
|
||||
|
||||
}
|
||||
|
|
@ -406,13 +406,13 @@ object service_spec = {
|
|||
relation responded(X:txid)
|
||||
|
||||
after init {
|
||||
responded(X) := false;
|
||||
responded(X) := false;
|
||||
}
|
||||
|
||||
before cl_chans.send(p : client_id, m : response.t) {
|
||||
assert ~responded(m.tx);
|
||||
assert m.bd = ref.eval(m.tx);
|
||||
responded(m.tx) := true;
|
||||
assert ~responded(m.tx);
|
||||
assert m.bd = ref.eval(m.tx);
|
||||
responded(m.tx) := true;
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -427,7 +427,7 @@ object mid_spec = {
|
|||
instance queue : unbounded_queue(txid)
|
||||
|
||||
after ser.serialize(tx:txid) {
|
||||
call queue.push(tx);
|
||||
call queue.push(tx);
|
||||
}
|
||||
|
||||
# When a message is received at the secondary on the forward
|
||||
|
|
@ -437,8 +437,8 @@ object mid_spec = {
|
|||
# serialization order).
|
||||
|
||||
before fwd_chan.rcvr.recv(inp : req_msg) {
|
||||
assert inp.req.bd = ref.txs(inp.req.tx);
|
||||
assert inp.req.tx = queue.pop;
|
||||
assert inp.req.bd = ref.txs(inp.req.tx);
|
||||
assert inp.req.tx = queue.pop;
|
||||
}
|
||||
|
||||
# This tells IVy that the above specification is a guarantee for
|
||||
|
|
@ -458,7 +458,7 @@ object mid_spec = {
|
|||
relation acked(X:txid)
|
||||
|
||||
after init {
|
||||
acked(X) := false;
|
||||
acked(X) := false;
|
||||
}
|
||||
|
||||
# When an ack message is sent on the reverse channel, it must have
|
||||
|
|
@ -467,10 +467,10 @@ object mid_spec = {
|
|||
# fact that it is now acked.
|
||||
|
||||
before rev_chan.sndr.send(inp : req_msg) {
|
||||
assert ref.committed(inp.req.tx);
|
||||
assert ref.txs(inp.req.tx) = inp.req.bd;
|
||||
assert ~acked(inp.req.tx);
|
||||
acked(inp.req.tx) := true;
|
||||
assert ref.committed(inp.req.tx);
|
||||
assert ref.txs(inp.req.tx) = inp.req.bd;
|
||||
assert ~acked(inp.req.tx);
|
||||
acked(inp.req.tx) := true;
|
||||
}
|
||||
|
||||
# When a request is created, we record the destination server. In
|
||||
|
|
@ -483,16 +483,16 @@ object mid_spec = {
|
|||
function req_dest(X:txid) : dest.t
|
||||
|
||||
after ref.create(inp : request_body.t, dst:dest.t) returns (tx : txid) {
|
||||
req_dest(tx) := dst
|
||||
req_dest(tx) := dst
|
||||
}
|
||||
|
||||
|
||||
# We now specify that all reads must be commited by the server
|
||||
# they are addressed to, while all writes are committed by the
|
||||
# secondary
|
||||
|
||||
before ref.commit(tx : txid,dst:dest.t) {
|
||||
assert ref.txs(tx).knd = read -> req_dest(tx) = dst;
|
||||
assert ref.txs(tx).knd = write -> dst = dest.sec
|
||||
assert ref.txs(tx).knd = read -> req_dest(tx) = dst;
|
||||
assert ref.txs(tx).knd = write -> dst = dest.sec
|
||||
}
|
||||
|
||||
}
|
||||
|
|
|
|||
|
|
@ -9,10 +9,7 @@ Project("{8BC9CEB8-8B4A-11D0-8D11-00A0C91BC942}") = "repstore2_sec", "repstore2_
|
|||
EndProject
|
||||
Global
|
||||
GlobalSection(SolutionConfigurationPlatforms) = preSolution
|
||||
Debug|x64 = Debug|x64
|
||||
Debug|x86 = Debug|x86
|
||||
Release|x64 = Release|x64
|
||||
Release|x86 = Release|x86
|
||||
EndGlobalSection
|
||||
GlobalSection(ProjectConfigurationPlatforms) = postSolution
|
||||
{A48A9407-CA01-4B56-8D51-303F4FC5F6E1}.Debug|x64.ActiveCfg = Debug|x64
|
||||
|
|
|
|||
|
|
@ -39,29 +39,29 @@ type request_kind = {write,read}
|
|||
|
||||
object request_body = {
|
||||
type t = struct {
|
||||
knd : request_kind,
|
||||
ky : key,
|
||||
vl : value
|
||||
knd : request_kind,
|
||||
ky : key,
|
||||
vl : value
|
||||
}
|
||||
}
|
||||
|
||||
object request = {
|
||||
type t = struct {
|
||||
tx : txid,
|
||||
bd : request_body.t
|
||||
tx : txid,
|
||||
bd : request_body.t
|
||||
}
|
||||
}
|
||||
|
||||
object response_body = {
|
||||
type t = struct {
|
||||
vl : value
|
||||
vl : value
|
||||
}
|
||||
}
|
||||
|
||||
object response = {
|
||||
type t = struct {
|
||||
tx : txid,
|
||||
bd : response_body.t
|
||||
tx : txid,
|
||||
bd : response_body.t
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -70,15 +70,15 @@ object response = {
|
|||
module replica = {
|
||||
function store(K:key) : value
|
||||
after init {
|
||||
store(K) := 0
|
||||
store(K) := 0
|
||||
}
|
||||
action exec(inp : request_body.t) returns (out:response_body.t) = {
|
||||
if inp.knd = write {
|
||||
store(inp.ky) := inp.vl;
|
||||
}
|
||||
else if inp.knd = read {
|
||||
out.vl := store(inp.ky);
|
||||
}
|
||||
if inp.knd = write {
|
||||
store(inp.ky) := inp.vl;
|
||||
}
|
||||
else if inp.knd = read {
|
||||
out.vl := store(inp.ky);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -108,27 +108,27 @@ object ref = {
|
|||
relation committed(X:txid)
|
||||
|
||||
after init {
|
||||
next := 0;
|
||||
committed(X) := false;
|
||||
next := 0;
|
||||
committed(X) := false;
|
||||
}
|
||||
|
||||
implement create {
|
||||
tx := next;
|
||||
txs(tx) := inp;
|
||||
next := next + 1;
|
||||
tx := next;
|
||||
txs(tx) := inp;
|
||||
next := next + 1;
|
||||
}
|
||||
|
||||
implement commit {
|
||||
assert 0 <= tx & tx < next;
|
||||
assert ~committed(tx);
|
||||
txres(tx) := rep.exec(txs(tx));
|
||||
committed(tx) := true;
|
||||
assert 0 <= tx & tx < next;
|
||||
assert ~committed(tx);
|
||||
txres(tx) := rep.exec(txs(tx));
|
||||
committed(tx) := true;
|
||||
}
|
||||
delegate commit
|
||||
|
||||
implement eval {
|
||||
assert committed(tx);
|
||||
res := txres(tx);
|
||||
assert committed(tx);
|
||||
res := txres(tx);
|
||||
}
|
||||
delegate eval
|
||||
|
||||
|
|
@ -152,7 +152,7 @@ object ser = {
|
|||
relation serialized(X:txid)
|
||||
|
||||
after init {
|
||||
serialized(X) := false;
|
||||
serialized(X) := false;
|
||||
}
|
||||
|
||||
# To serialzie a write, we must guarantee that transaction exists,
|
||||
|
|
@ -160,10 +160,10 @@ object ser = {
|
|||
# only serialize write transactions.
|
||||
|
||||
implement serialize {
|
||||
assert 0 <= tx & tx < ref.next;
|
||||
assert ~serialized(tx);
|
||||
assert ref.txs(tx).knd = write;
|
||||
serialized(tx) := true;
|
||||
assert 0 <= tx & tx < ref.next;
|
||||
assert ~serialized(tx);
|
||||
assert ref.txs(tx).knd = write;
|
||||
serialized(tx) := true;
|
||||
}
|
||||
delegate serialize
|
||||
|
||||
|
|
@ -171,7 +171,7 @@ object ser = {
|
|||
# until it is serialized.
|
||||
|
||||
before ref.commit(tx : txid,dst:dest.t) {
|
||||
assert ref.txs(tx).knd = write -> serialized(tx);
|
||||
assert ref.txs(tx).knd = write -> serialized(tx);
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -212,15 +212,15 @@ module client(cid,prim_chan,sec_chan,cl_chans) = {
|
|||
# parameter `the_dst`.
|
||||
|
||||
implement client_request {
|
||||
var m : req_msg;
|
||||
m.cid := cid;
|
||||
m.req.tx := ref.create(req,the_dst);
|
||||
m.req.bd := req;
|
||||
if the_dst = dest.prim {
|
||||
call prim_chan.send(m);
|
||||
} else {
|
||||
call sec_chan.send(m);
|
||||
}
|
||||
var m : req_msg;
|
||||
m.cid := cid;
|
||||
m.req.tx := ref.create(req,the_dst);
|
||||
m.req.bd := req;
|
||||
if the_dst = dest.prim {
|
||||
call prim_chan.send(m);
|
||||
} else {
|
||||
call sec_chan.send(m);
|
||||
}
|
||||
}
|
||||
|
||||
# To handle a response from the server, we simply pass it to the
|
||||
|
|
@ -228,7 +228,7 @@ module client(cid,prim_chan,sec_chan,cl_chans) = {
|
|||
# "ghost" and is only used for specification.
|
||||
|
||||
implement cl_chans.recv(resp : response.t) {
|
||||
call client_response(resp.bd,resp.tx)
|
||||
call client_response(resp.bd,resp.tx)
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -252,9 +252,9 @@ module primary_node(port, fwd_chan, rev_chan, cl_chans) = {
|
|||
# Initially, all the counters are zero.
|
||||
|
||||
after init {
|
||||
pending(K) := 0;
|
||||
pending(K) := 0;
|
||||
}
|
||||
|
||||
|
||||
# When receiving a request message from a client, the primary
|
||||
# node must first check whether it is a read or a write. In the case
|
||||
# of a read, we check if the key has a pending write. If not, we commit
|
||||
|
|
@ -265,32 +265,32 @@ module primary_node(port, fwd_chan, rev_chan, cl_chans) = {
|
|||
#
|
||||
|
||||
implement req_chan.recv(inp : req_msg) {
|
||||
var rr := inp.req.bd;
|
||||
var rr := inp.req.bd;
|
||||
if rr.knd = read {
|
||||
if pending(rr.ky) = 0 {
|
||||
call ref.commit(inp.req.tx,dest.prim);
|
||||
var res : response.t;
|
||||
res.tx := inp.req.tx;
|
||||
res.bd := rep.exec(rr);
|
||||
call cl_chans(inp.cid).send(res)
|
||||
} else {
|
||||
if pending(rr.ky) = 0 {
|
||||
call ref.commit(inp.req.tx,dest.prim);
|
||||
var res : response.t;
|
||||
res.tx := inp.req.tx;
|
||||
res.bd := rep.exec(rr);
|
||||
call cl_chans(inp.cid).send(res)
|
||||
} else {
|
||||
call req_chan.send(inp); # if cannot execute, recirculate
|
||||
}
|
||||
} else if rr.knd = write {
|
||||
call ser.serialize(inp.req.tx); # this is ghost!
|
||||
call fwd_chan.send(inp);
|
||||
var res := rep.exec(inp.req.bd);
|
||||
}
|
||||
}
|
||||
} else if rr.knd = write {
|
||||
call ser.serialize(inp.req.tx); # this is ghost!
|
||||
call fwd_chan.send(inp);
|
||||
var res := rep.exec(inp.req.bd);
|
||||
}
|
||||
}
|
||||
|
||||
# When we receive a write request on the acknowledgement channel,
|
||||
# we decrement the pending count of the key.
|
||||
|
||||
implement rev_chan.recv(inp : req_msg) {
|
||||
var rr := inp.req.bd;
|
||||
if rr.knd = write {
|
||||
pending(rr.ky) := pending(rr.ky).prev;
|
||||
}
|
||||
var rr := inp.req.bd;
|
||||
if rr.knd = write {
|
||||
pending(rr.ky) := pending(rr.ky).prev;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -304,16 +304,16 @@ module secondary_node(port, fwd_chan, rev_chan, cl_chans) = {
|
|||
instance rep : replica
|
||||
|
||||
instance req_chan : nondup_endpoint(port,req_msg)
|
||||
|
||||
|
||||
implement req_chan.recv(inp : req_msg) {
|
||||
var rr := inp.req.bd;
|
||||
var rr := inp.req.bd;
|
||||
if rr.knd = read {
|
||||
var res : response.t;
|
||||
res.tx := inp.req.tx;
|
||||
res.bd := rep.exec(rr);
|
||||
call cl_chans(inp.cid).send(res);
|
||||
}
|
||||
# ignore writes!
|
||||
var res : response.t;
|
||||
res.tx := inp.req.tx;
|
||||
res.bd := rep.exec(rr);
|
||||
call cl_chans(inp.cid).send(res);
|
||||
}
|
||||
# ignore writes!
|
||||
}
|
||||
|
||||
# When the secondary receives a forwarded write from the primary,
|
||||
|
|
@ -322,11 +322,11 @@ module secondary_node(port, fwd_chan, rev_chan, cl_chans) = {
|
|||
#
|
||||
|
||||
implement fwd_chan.recv(inp : req_msg) {
|
||||
var res : response.t;
|
||||
res.tx := inp.req.tx;
|
||||
res.bd := rep.exec(inp.req.bd);
|
||||
call cl_chans(inp.cid).send(res);
|
||||
call rev_chan.send(inp);
|
||||
var res : response.t;
|
||||
res.tx := inp.req.tx;
|
||||
res.bd := rep.exec(inp.req.bd);
|
||||
call cl_chans(inp.cid).send(res);
|
||||
call rev_chan.send(inp);
|
||||
}
|
||||
|
||||
}
|
||||
|
|
@ -371,13 +371,13 @@ object service_spec = {
|
|||
relation responded(X:txid)
|
||||
|
||||
after init {
|
||||
responded(X) := false;
|
||||
responded(X) := false;
|
||||
}
|
||||
|
||||
before cl_chans.send(p : client_id, m : response.t) {
|
||||
assert ~responded(m.tx);
|
||||
assert m.bd = ref.eval(m.tx);
|
||||
responded(m.tx) := true;
|
||||
assert ~responded(m.tx);
|
||||
assert m.bd = ref.eval(m.tx);
|
||||
responded(m.tx) := true;
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -392,7 +392,7 @@ object mid_spec = {
|
|||
instance queue : unbounded_queue(txid)
|
||||
|
||||
after ser.serialize(tx:txid) {
|
||||
call queue.push(tx);
|
||||
call queue.push(tx);
|
||||
}
|
||||
|
||||
# When a message is received at the secondary on the forward
|
||||
|
|
@ -408,9 +408,9 @@ object mid_spec = {
|
|||
# convenient.
|
||||
|
||||
before fwd_chan.rcvr.recv(inp : req_msg) {
|
||||
assert inp.req.bd = ref.txs(inp.req.tx);
|
||||
assert inp.req.tx = queue.pop;
|
||||
call ref.commit(inp.req.tx,dest.sec);
|
||||
assert inp.req.bd = ref.txs(inp.req.tx);
|
||||
assert inp.req.tx = queue.pop;
|
||||
call ref.commit(inp.req.tx,dest.sec);
|
||||
}
|
||||
|
||||
# This tells IVy that the above specification is a guarantee for
|
||||
|
|
@ -430,7 +430,7 @@ object mid_spec = {
|
|||
relation acked(X:txid)
|
||||
|
||||
after init {
|
||||
acked(X) := false;
|
||||
acked(X) := false;
|
||||
}
|
||||
|
||||
# When an ack message is sent on the reverse channel, must have
|
||||
|
|
@ -439,10 +439,10 @@ object mid_spec = {
|
|||
# record the fact that it is now acked.
|
||||
|
||||
before rev_chan.sndr.send(inp : req_msg) {
|
||||
assert ref.txs(inp.req.tx) = inp.req.bd;
|
||||
assert ref.committed(inp.req.tx);
|
||||
assert ~acked(inp.req.tx);
|
||||
acked(inp.req.tx) := true;
|
||||
assert ref.txs(inp.req.tx) = inp.req.bd;
|
||||
assert ref.committed(inp.req.tx);
|
||||
assert ~acked(inp.req.tx);
|
||||
acked(inp.req.tx) := true;
|
||||
}
|
||||
|
||||
# When a request is created, we record the destination server. In
|
||||
|
|
@ -455,24 +455,24 @@ object mid_spec = {
|
|||
function req_dest(X:txid) : dest.t
|
||||
|
||||
after ref.create(inp : request_body.t, dst:dest.t) returns (tx : txid) {
|
||||
req_dest(tx) := dst
|
||||
req_dest(tx) := dst
|
||||
}
|
||||
|
||||
|
||||
# We now specify that all reads must be commited by the server
|
||||
# they are addressed to, while all writes are committed by the
|
||||
# secondary
|
||||
|
||||
before ref.commit(tx : txid,dst:dest.t) {
|
||||
assert ref.txs(tx).knd = read -> req_dest(tx) = dst;
|
||||
assert ref.txs(tx).knd = write -> dst = dest.sec
|
||||
assert ref.txs(tx).knd = read -> req_dest(tx) = dst;
|
||||
assert ref.txs(tx).knd = write -> dst = dest.sec
|
||||
}
|
||||
|
||||
# Commit immediately all read requests from client to secondary
|
||||
|
||||
before sec.req_chan.recv(inp : req_msg) {
|
||||
if inp.req.bd.knd = read {
|
||||
call ref.commit(inp.req.tx,dest.sec)
|
||||
}
|
||||
if inp.req.bd.knd = read {
|
||||
call ref.commit(inp.req.tx,dest.sec)
|
||||
}
|
||||
}
|
||||
|
||||
}
|
||||
|
|
|
|||
|
|
@ -9,10 +9,7 @@ Project("{8BC9CEB8-8B4A-11D0-8D11-00A0C91BC942}") = "repstore2bug_sec", "repstor
|
|||
EndProject
|
||||
Global
|
||||
GlobalSection(SolutionConfigurationPlatforms) = preSolution
|
||||
Debug|x64 = Debug|x64
|
||||
Debug|x86 = Debug|x86
|
||||
Release|x64 = Release|x64
|
||||
Release|x86 = Release|x86
|
||||
EndGlobalSection
|
||||
GlobalSection(ProjectConfigurationPlatforms) = postSolution
|
||||
{A48A9407-CA01-4B56-8D51-303F4FC5F6E1}.Debug|x64.ActiveCfg = Debug|x64
|
||||
|
|
|
|||
|
|
@ -44,29 +44,29 @@ type request_kind = {write,read}
|
|||
|
||||
object request_body = {
|
||||
type t = struct {
|
||||
knd : request_kind,
|
||||
ky : key,
|
||||
vl : value
|
||||
knd : request_kind,
|
||||
ky : key,
|
||||
vl : value
|
||||
}
|
||||
}
|
||||
|
||||
object request = {
|
||||
type t = struct {
|
||||
tx : txid,
|
||||
bd : request_body.t
|
||||
tx : txid,
|
||||
bd : request_body.t
|
||||
}
|
||||
}
|
||||
|
||||
object response_body = {
|
||||
type t = struct {
|
||||
vl : value
|
||||
vl : value
|
||||
}
|
||||
}
|
||||
|
||||
object response = {
|
||||
type t = struct {
|
||||
tx : txid,
|
||||
bd : response_body.t
|
||||
tx : txid,
|
||||
bd : response_body.t
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -75,15 +75,15 @@ object response = {
|
|||
module replica = {
|
||||
function store(K:key) : value
|
||||
after init {
|
||||
store(K) := 0
|
||||
store(K) := 0
|
||||
}
|
||||
action exec(inp : request_body.t) returns (out:response_body.t) = {
|
||||
if inp.knd = write {
|
||||
store(inp.ky) := inp.vl;
|
||||
}
|
||||
else if inp.knd = read {
|
||||
out.vl := store(inp.ky);
|
||||
}
|
||||
if inp.knd = write {
|
||||
store(inp.ky) := inp.vl;
|
||||
}
|
||||
else if inp.knd = read {
|
||||
out.vl := store(inp.ky);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -113,27 +113,27 @@ object ref = {
|
|||
relation committed(X:txid)
|
||||
|
||||
after init {
|
||||
next := 0;
|
||||
committed(X) := false;
|
||||
next := 0;
|
||||
committed(X) := false;
|
||||
}
|
||||
|
||||
implement create {
|
||||
tx := next;
|
||||
txs(tx) := inp;
|
||||
next := next + 1;
|
||||
tx := next;
|
||||
txs(tx) := inp;
|
||||
next := next + 1;
|
||||
}
|
||||
|
||||
implement commit {
|
||||
assert 0 <= tx & tx < next;
|
||||
assert ~committed(tx);
|
||||
txres(tx) := rep.exec(txs(tx));
|
||||
committed(tx) := true;
|
||||
assert 0 <= tx & tx < next;
|
||||
assert ~committed(tx);
|
||||
txres(tx) := rep.exec(txs(tx));
|
||||
committed(tx) := true;
|
||||
}
|
||||
delegate commit
|
||||
|
||||
implement eval {
|
||||
assert committed(tx);
|
||||
res := txres(tx);
|
||||
assert committed(tx);
|
||||
res := txres(tx);
|
||||
}
|
||||
delegate eval
|
||||
|
||||
|
|
@ -157,7 +157,7 @@ object ser = {
|
|||
relation serialized(X:txid)
|
||||
|
||||
after init {
|
||||
serialized(X) := false;
|
||||
serialized(X) := false;
|
||||
}
|
||||
|
||||
# To serialzie a write, we must guarantee that transaction exists,
|
||||
|
|
@ -165,10 +165,10 @@ object ser = {
|
|||
# only serialize write transactions.
|
||||
|
||||
implement serialize {
|
||||
assert 0 <= tx & tx < ref.next;
|
||||
assert ~serialized(tx);
|
||||
assert ref.txs(tx).knd = write;
|
||||
serialized(tx) := true;
|
||||
assert 0 <= tx & tx < ref.next;
|
||||
assert ~serialized(tx);
|
||||
assert ref.txs(tx).knd = write;
|
||||
serialized(tx) := true;
|
||||
}
|
||||
delegate serialize
|
||||
|
||||
|
|
@ -176,7 +176,7 @@ object ser = {
|
|||
# until it is serialized.
|
||||
|
||||
before ref.commit(tx : txid,dst:dest.t) {
|
||||
assert ref.txs(tx).knd = write -> serialized(tx);
|
||||
assert ref.txs(tx).knd = write -> serialized(tx);
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -217,15 +217,15 @@ module client(cid,prim_chan,sec_chan,cl_chans) = {
|
|||
# parameter `the_dst`.
|
||||
|
||||
implement client_request {
|
||||
var m : req_msg;
|
||||
m.cid := cid;
|
||||
m.req.tx := ref.create(req,the_dst);
|
||||
m.req.bd := req;
|
||||
if the_dst = dest.prim {
|
||||
call prim_chan.send(m);
|
||||
} else {
|
||||
call sec_chan.send(m);
|
||||
}
|
||||
var m : req_msg;
|
||||
m.cid := cid;
|
||||
m.req.tx := ref.create(req,the_dst);
|
||||
m.req.bd := req;
|
||||
if the_dst = dest.prim {
|
||||
call prim_chan.send(m);
|
||||
} else {
|
||||
call sec_chan.send(m);
|
||||
}
|
||||
}
|
||||
|
||||
# To handle a response from the server, we simply pass it to the
|
||||
|
|
@ -233,7 +233,7 @@ module client(cid,prim_chan,sec_chan,cl_chans) = {
|
|||
# "ghost" and is only used for specification.
|
||||
|
||||
implement cl_chans.recv(resp : response.t) {
|
||||
call client_response(resp.bd,resp.tx)
|
||||
call client_response(resp.bd,resp.tx)
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -257,9 +257,9 @@ module primary_node(port, fwd_chan, rev_chan, cl_chans) = {
|
|||
# Initially, all the counters are zero.
|
||||
|
||||
after init {
|
||||
pending(K) := 0;
|
||||
pending(K) := 0;
|
||||
}
|
||||
|
||||
|
||||
# When receiving a request message from a client, the primary
|
||||
# node must first check whether it is a read or a write. In the case
|
||||
# of a read, we check if the key has a pending write. If not, we commit
|
||||
|
|
@ -270,33 +270,33 @@ module primary_node(port, fwd_chan, rev_chan, cl_chans) = {
|
|||
#
|
||||
|
||||
implement req_chan.recv(inp : req_msg) {
|
||||
var rr := inp.req.bd;
|
||||
var rr := inp.req.bd;
|
||||
if rr.knd = read {
|
||||
if pending(rr.ky) = 0 {
|
||||
call ref.commit(inp.req.tx,dest.prim);
|
||||
var res : response.t;
|
||||
res.tx := inp.req.tx;
|
||||
res.bd := rep.exec(rr);
|
||||
call cl_chans(inp.cid).send(res)
|
||||
} else {
|
||||
if pending(rr.ky) = 0 {
|
||||
call ref.commit(inp.req.tx,dest.prim);
|
||||
var res : response.t;
|
||||
res.tx := inp.req.tx;
|
||||
res.bd := rep.exec(rr);
|
||||
call cl_chans(inp.cid).send(res)
|
||||
} else {
|
||||
call req_chan.send(inp); # if cannot execute, recirculate (HINT)
|
||||
}
|
||||
} else if rr.knd = write {
|
||||
call ser.serialize(inp.req.tx); # this is ghost!
|
||||
call fwd_chan.send(inp);
|
||||
pending(rr.ky) := pending(rr.ky).next;
|
||||
var res := rep.exec(inp.req.bd);
|
||||
}
|
||||
}
|
||||
} else if rr.knd = write {
|
||||
call ser.serialize(inp.req.tx); # this is ghost!
|
||||
call fwd_chan.send(inp);
|
||||
pending(rr.ky) := pending(rr.ky).next;
|
||||
var res := rep.exec(inp.req.bd);
|
||||
}
|
||||
}
|
||||
|
||||
# When we receive a write request on the acknowledgement channel,
|
||||
# we decrement the pending count of the key.
|
||||
|
||||
implement rev_chan.recv(inp : req_msg) {
|
||||
var rr := inp.req.bd;
|
||||
if rr.knd = write {
|
||||
pending(rr.ky) := pending(rr.ky).prev;
|
||||
}
|
||||
var rr := inp.req.bd;
|
||||
if rr.knd = write {
|
||||
pending(rr.ky) := pending(rr.ky).prev;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -310,16 +310,16 @@ module secondary_node(port, fwd_chan, rev_chan, cl_chans) = {
|
|||
instance rep : replica
|
||||
|
||||
instance req_chan : nondup_endpoint(port,req_msg)
|
||||
|
||||
|
||||
implement req_chan.recv(inp : req_msg) {
|
||||
var rr := inp.req.bd;
|
||||
var rr := inp.req.bd;
|
||||
if rr.knd = read {
|
||||
var res : response.t;
|
||||
res.tx := inp.req.tx;
|
||||
res.bd := rep.exec(rr);
|
||||
call cl_chans(inp.cid).send(res);
|
||||
}
|
||||
# ignore writes!
|
||||
var res : response.t;
|
||||
res.tx := inp.req.tx;
|
||||
res.bd := rep.exec(rr);
|
||||
call cl_chans(inp.cid).send(res);
|
||||
}
|
||||
# ignore writes!
|
||||
}
|
||||
|
||||
# When the secondary receives a forwarded write from the primary,
|
||||
|
|
@ -331,11 +331,11 @@ module secondary_node(port, fwd_chan, rev_chan, cl_chans) = {
|
|||
|
||||
# HINT: do something here (see req_chan.recv above)
|
||||
|
||||
var res : response.t;
|
||||
res.tx := inp.req.tx;
|
||||
res.bd := rep.exec(inp.req.bd);
|
||||
call cl_chans(inp.cid).send(res);
|
||||
call rev_chan.send(inp);
|
||||
var res : response.t;
|
||||
res.tx := inp.req.tx;
|
||||
res.bd := rep.exec(inp.req.bd);
|
||||
call cl_chans(inp.cid).send(res);
|
||||
call rev_chan.send(inp);
|
||||
}
|
||||
|
||||
}
|
||||
|
|
@ -380,13 +380,13 @@ object service_spec = {
|
|||
relation responded(X:txid)
|
||||
|
||||
after init {
|
||||
responded(X) := false;
|
||||
responded(X) := false;
|
||||
}
|
||||
|
||||
before cl_chans.send(p : client_id, m : response.t) {
|
||||
assert ~responded(m.tx);
|
||||
assert m.bd = ref.eval(m.tx);
|
||||
responded(m.tx) := true;
|
||||
assert ~responded(m.tx);
|
||||
assert m.bd = ref.eval(m.tx);
|
||||
responded(m.tx) := true;
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -401,7 +401,7 @@ object mid_spec = {
|
|||
instance queue : unbounded_queue(txid)
|
||||
|
||||
after ser.serialize(tx:txid) {
|
||||
call queue.push(tx);
|
||||
call queue.push(tx);
|
||||
}
|
||||
|
||||
# When a message is received at the secondary on the forward
|
||||
|
|
@ -417,9 +417,9 @@ object mid_spec = {
|
|||
# convenient.
|
||||
|
||||
before fwd_chan.rcvr.recv(inp : req_msg) {
|
||||
assert inp.req.bd = ref.txs(inp.req.tx);
|
||||
assert inp.req.tx = queue.pop;
|
||||
call ref.commit(inp.req.tx,dest.sec);
|
||||
assert inp.req.bd = ref.txs(inp.req.tx);
|
||||
assert inp.req.tx = queue.pop;
|
||||
call ref.commit(inp.req.tx,dest.sec);
|
||||
}
|
||||
|
||||
# This tells IVy that the above specification is a guarantee for
|
||||
|
|
@ -439,7 +439,7 @@ object mid_spec = {
|
|||
relation acked(X:txid)
|
||||
|
||||
after init {
|
||||
acked(X) := false;
|
||||
acked(X) := false;
|
||||
}
|
||||
|
||||
# When an ack message is sent on the reverse channel, it must have
|
||||
|
|
@ -448,10 +448,10 @@ object mid_spec = {
|
|||
# fact that it is now acked.
|
||||
|
||||
before rev_chan.sndr.send(inp : req_msg) {
|
||||
assert ref.committed(inp.req.tx);
|
||||
assert ref.txs(inp.req.tx) = inp.req.bd;
|
||||
assert ~acked(inp.req.tx);
|
||||
acked(inp.req.tx) := true;
|
||||
assert ref.committed(inp.req.tx);
|
||||
assert ref.txs(inp.req.tx) = inp.req.bd;
|
||||
assert ~acked(inp.req.tx);
|
||||
acked(inp.req.tx) := true;
|
||||
}
|
||||
|
||||
# When a request is created, we record the destination server. In
|
||||
|
|
@ -467,24 +467,24 @@ object mid_spec = {
|
|||
function req_dest(X:txid) : dest.t
|
||||
|
||||
after ref.create(inp : request_body.t, dst:dest.t) returns (tx : txid) {
|
||||
req_dest(tx) := dst
|
||||
req_dest(tx) := dst
|
||||
}
|
||||
|
||||
|
||||
# We now specify that all reads must be commited by the server
|
||||
# they are addressed to, while all writes are committed by the
|
||||
# secondary
|
||||
|
||||
before ref.commit(tx : txid,dst:dest.t) {
|
||||
assert ref.txs(tx).knd = read -> req_dest(tx) = dst;
|
||||
assert ref.txs(tx).knd = write -> dst = dest.sec
|
||||
assert ref.txs(tx).knd = read -> req_dest(tx) = dst;
|
||||
assert ref.txs(tx).knd = write -> dst = dest.sec
|
||||
}
|
||||
|
||||
# Commit immediately all read requests from client to secondary
|
||||
|
||||
before sec.req_chan.recv(inp : req_msg) {
|
||||
if inp.req.bd.knd = read {
|
||||
call ref.commit(inp.req.tx,dest.sec)
|
||||
}
|
||||
if inp.req.bd.knd = read {
|
||||
call ref.commit(inp.req.tx,dest.sec)
|
||||
}
|
||||
}
|
||||
|
||||
}
|
||||
|
|
|
|||
|
|
@ -9,10 +9,7 @@ Project("{8BC9CEB8-8B4A-11D0-8D11-00A0C91BC942}") = "repstore2ex_sec", "repstore
|
|||
EndProject
|
||||
Global
|
||||
GlobalSection(SolutionConfigurationPlatforms) = preSolution
|
||||
Debug|x64 = Debug|x64
|
||||
Debug|x86 = Debug|x86
|
||||
Release|x64 = Release|x64
|
||||
Release|x86 = Release|x86
|
||||
EndGlobalSection
|
||||
GlobalSection(ProjectConfigurationPlatforms) = postSolution
|
||||
{A48A9407-CA01-4B56-8D51-303F4FC5F6E1}.Debug|x64.ActiveCfg = Debug|x64
|
||||
|
|
|
|||
|
|
@ -44,29 +44,29 @@ type request_kind = {write,read}
|
|||
|
||||
object request_body = {
|
||||
type t = struct {
|
||||
knd : request_kind,
|
||||
ky : key,
|
||||
vl : value
|
||||
knd : request_kind,
|
||||
ky : key,
|
||||
vl : value
|
||||
}
|
||||
}
|
||||
|
||||
object request = {
|
||||
type t = struct {
|
||||
tx : txid,
|
||||
bd : request_body.t
|
||||
tx : txid,
|
||||
bd : request_body.t
|
||||
}
|
||||
}
|
||||
|
||||
object response_body = {
|
||||
type t = struct {
|
||||
vl : value
|
||||
vl : value
|
||||
}
|
||||
}
|
||||
|
||||
object response = {
|
||||
type t = struct {
|
||||
tx : txid,
|
||||
bd : response_body.t
|
||||
tx : txid,
|
||||
bd : response_body.t
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -75,15 +75,15 @@ object response = {
|
|||
module replica = {
|
||||
function store(K:key) : value
|
||||
after init {
|
||||
store(K) := 0
|
||||
store(K) := 0
|
||||
}
|
||||
action exec(inp : request_body.t) returns (out:response_body.t) = {
|
||||
if inp.knd = write {
|
||||
store(inp.ky) := inp.vl;
|
||||
}
|
||||
else if inp.knd = read {
|
||||
out.vl := store(inp.ky);
|
||||
}
|
||||
if inp.knd = write {
|
||||
store(inp.ky) := inp.vl;
|
||||
}
|
||||
else if inp.knd = read {
|
||||
out.vl := store(inp.ky);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -113,27 +113,27 @@ object ref = {
|
|||
relation committed(X:txid)
|
||||
|
||||
after init {
|
||||
next := 0;
|
||||
committed(X) := false;
|
||||
next := 0;
|
||||
committed(X) := false;
|
||||
}
|
||||
|
||||
implement create {
|
||||
tx := next;
|
||||
txs(tx) := inp;
|
||||
next := next + 1;
|
||||
tx := next;
|
||||
txs(tx) := inp;
|
||||
next := next + 1;
|
||||
}
|
||||
|
||||
implement commit {
|
||||
assert 0 <= tx & tx < next;
|
||||
assert ~committed(tx);
|
||||
txres(tx) := rep.exec(txs(tx));
|
||||
committed(tx) := true;
|
||||
assert 0 <= tx & tx < next;
|
||||
assert ~committed(tx);
|
||||
txres(tx) := rep.exec(txs(tx));
|
||||
committed(tx) := true;
|
||||
}
|
||||
delegate commit
|
||||
|
||||
implement eval {
|
||||
assert committed(tx);
|
||||
res := txres(tx);
|
||||
assert committed(tx);
|
||||
res := txres(tx);
|
||||
}
|
||||
delegate eval
|
||||
|
||||
|
|
@ -157,7 +157,7 @@ object ser = {
|
|||
relation serialized(X:txid)
|
||||
|
||||
after init {
|
||||
serialized(X) := false;
|
||||
serialized(X) := false;
|
||||
}
|
||||
|
||||
# To serialzie a write, we must guarantee that transaction exists,
|
||||
|
|
@ -165,10 +165,10 @@ object ser = {
|
|||
# only serialize write transactions.
|
||||
|
||||
implement serialize {
|
||||
assert 0 <= tx & tx < ref.next;
|
||||
assert ~serialized(tx);
|
||||
assert ref.txs(tx).knd = write;
|
||||
serialized(tx) := true;
|
||||
assert 0 <= tx & tx < ref.next;
|
||||
assert ~serialized(tx);
|
||||
assert ref.txs(tx).knd = write;
|
||||
serialized(tx) := true;
|
||||
}
|
||||
delegate serialize
|
||||
|
||||
|
|
@ -176,7 +176,7 @@ object ser = {
|
|||
# until it is serialized.
|
||||
|
||||
before ref.commit(tx : txid,dst:dest.t) {
|
||||
assert ref.txs(tx).knd = write -> serialized(tx);
|
||||
assert ref.txs(tx).knd = write -> serialized(tx);
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -217,15 +217,15 @@ module client(cid,prim_chan,sec_chan,cl_chans) = {
|
|||
# parameter `the_dst`.
|
||||
|
||||
implement client_request {
|
||||
var m : req_msg;
|
||||
m.cid := cid;
|
||||
m.req.tx := ref.create(req,the_dst);
|
||||
m.req.bd := req;
|
||||
if the_dst = dest.prim {
|
||||
call prim_chan.send(m);
|
||||
} else {
|
||||
call sec_chan.send(m);
|
||||
}
|
||||
var m : req_msg;
|
||||
m.cid := cid;
|
||||
m.req.tx := ref.create(req,the_dst);
|
||||
m.req.bd := req;
|
||||
if the_dst = dest.prim {
|
||||
call prim_chan.send(m);
|
||||
} else {
|
||||
call sec_chan.send(m);
|
||||
}
|
||||
}
|
||||
|
||||
# To handle a response from the server, we simply pass it to the
|
||||
|
|
@ -233,7 +233,7 @@ module client(cid,prim_chan,sec_chan,cl_chans) = {
|
|||
# "ghost" and is only used for specification.
|
||||
|
||||
implement cl_chans.recv(resp : response.t) {
|
||||
call client_response(resp.bd,resp.tx)
|
||||
call client_response(resp.bd,resp.tx)
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -257,9 +257,9 @@ module primary_node(port, fwd_chan, rev_chan, cl_chans) = {
|
|||
# Initially, all the counters are zero.
|
||||
|
||||
after init {
|
||||
pending(K) := 0;
|
||||
pending(K) := 0;
|
||||
}
|
||||
|
||||
|
||||
# When receiving a request message from a client, the primary
|
||||
# node must first check whether it is a read or a write. In the case
|
||||
# of a read, we check if the key has a pending write. If not, we commit
|
||||
|
|
@ -270,36 +270,36 @@ module primary_node(port, fwd_chan, rev_chan, cl_chans) = {
|
|||
#
|
||||
|
||||
implement req_chan.recv(inp : req_msg) {
|
||||
var rr := inp.req.bd;
|
||||
var rr := inp.req.bd;
|
||||
if rr.knd = read {
|
||||
if pending(rr.ky) = 0 {
|
||||
call ref.commit(inp.req.tx,dest.prim);
|
||||
var res : response.t;
|
||||
res.tx := inp.req.tx;
|
||||
res.bd := rep.exec(rr);
|
||||
call cl_chans(inp.cid).send(res)
|
||||
} else {
|
||||
if pending(rr.ky) = 0 {
|
||||
call ref.commit(inp.req.tx,dest.prim);
|
||||
var res : response.t;
|
||||
res.tx := inp.req.tx;
|
||||
res.bd := rep.exec(rr);
|
||||
call cl_chans(inp.cid).send(res)
|
||||
} else {
|
||||
|
||||
# SOLN: if can't read, send on `fwd_chan`
|
||||
|
||||
# SOLN: if can't read, send on `fwd_chan`
|
||||
|
||||
call fwd_chan.send(inp);
|
||||
}
|
||||
} else if rr.knd = write {
|
||||
call ser.serialize(inp.req.tx); # this is ghost!
|
||||
call fwd_chan.send(inp);
|
||||
pending(rr.ky) := pending(rr.ky).next;
|
||||
var res := rep.exec(inp.req.bd);
|
||||
}
|
||||
}
|
||||
} else if rr.knd = write {
|
||||
call ser.serialize(inp.req.tx); # this is ghost!
|
||||
call fwd_chan.send(inp);
|
||||
pending(rr.ky) := pending(rr.ky).next;
|
||||
var res := rep.exec(inp.req.bd);
|
||||
}
|
||||
}
|
||||
|
||||
# When we receive a write request on the acknowledgement channel,
|
||||
# we decrement the pending count of the key.
|
||||
|
||||
implement rev_chan.recv(inp : req_msg) {
|
||||
var rr := inp.req.bd;
|
||||
if rr.knd = write {
|
||||
pending(rr.ky) := pending(rr.ky).prev;
|
||||
}
|
||||
var rr := inp.req.bd;
|
||||
if rr.knd = write {
|
||||
pending(rr.ky) := pending(rr.ky).prev;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -313,16 +313,16 @@ module secondary_node(port, fwd_chan, rev_chan, cl_chans) = {
|
|||
instance rep : replica
|
||||
|
||||
instance req_chan : nondup_endpoint(port,req_msg)
|
||||
|
||||
|
||||
implement req_chan.recv(inp : req_msg) {
|
||||
var rr := inp.req.bd;
|
||||
var rr := inp.req.bd;
|
||||
if rr.knd = read {
|
||||
var res : response.t;
|
||||
res.tx := inp.req.tx;
|
||||
res.bd := rep.exec(rr);
|
||||
call cl_chans(inp.cid).send(res);
|
||||
}
|
||||
# ignore writes!
|
||||
var res : response.t;
|
||||
res.tx := inp.req.tx;
|
||||
res.bd := rep.exec(rr);
|
||||
call cl_chans(inp.cid).send(res);
|
||||
}
|
||||
# ignore writes!
|
||||
}
|
||||
|
||||
# When the secondary receives a forwarded write from the primary,
|
||||
|
|
@ -334,20 +334,20 @@ module secondary_node(port, fwd_chan, rev_chan, cl_chans) = {
|
|||
|
||||
# SOLN: handle reads here just like above
|
||||
|
||||
var rr := inp.req.bd;
|
||||
var rr := inp.req.bd;
|
||||
if rr.knd = read {
|
||||
var res : response.t;
|
||||
res.tx := inp.req.tx;
|
||||
res.bd := rep.exec(rr);
|
||||
call cl_chans(inp.cid).send(res);
|
||||
}
|
||||
else {
|
||||
var res : response.t;
|
||||
res.tx := inp.req.tx;
|
||||
res.bd := rep.exec(inp.req.bd);
|
||||
call cl_chans(inp.cid).send(res);
|
||||
call rev_chan.send(inp);
|
||||
}
|
||||
var res : response.t;
|
||||
res.tx := inp.req.tx;
|
||||
res.bd := rep.exec(rr);
|
||||
call cl_chans(inp.cid).send(res);
|
||||
}
|
||||
else {
|
||||
var res : response.t;
|
||||
res.tx := inp.req.tx;
|
||||
res.bd := rep.exec(inp.req.bd);
|
||||
call cl_chans(inp.cid).send(res);
|
||||
call rev_chan.send(inp);
|
||||
}
|
||||
}
|
||||
|
||||
}
|
||||
|
|
@ -392,13 +392,13 @@ object service_spec = {
|
|||
relation responded(X:txid)
|
||||
|
||||
after init {
|
||||
responded(X) := false;
|
||||
responded(X) := false;
|
||||
}
|
||||
|
||||
before cl_chans.send(p : client_id, m : response.t) {
|
||||
assert ~responded(m.tx);
|
||||
assert m.bd = ref.eval(m.tx);
|
||||
responded(m.tx) := true;
|
||||
assert ~responded(m.tx);
|
||||
assert m.bd = ref.eval(m.tx);
|
||||
responded(m.tx) := true;
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -413,7 +413,7 @@ object mid_spec = {
|
|||
instance queue : unbounded_queue(txid)
|
||||
|
||||
after ser.serialize(tx:txid) {
|
||||
call queue.push(tx);
|
||||
call queue.push(tx);
|
||||
}
|
||||
|
||||
# When a message is received at the secondary on the forward
|
||||
|
|
@ -429,21 +429,21 @@ object mid_spec = {
|
|||
# convenient.
|
||||
|
||||
before fwd_chan.rcvr.recv(inp : req_msg) {
|
||||
assert inp.req.bd = ref.txs(inp.req.tx);
|
||||
assert inp.req.bd = ref.txs(inp.req.tx);
|
||||
|
||||
# SOLN: before commiting a read from the forwarding channel,
|
||||
# we need to change its destination. Else, the monitor for
|
||||
# `ref.commit` below will fail. In case of writes, we do as before.
|
||||
# SOLN: before commiting a read from the forwarding channel,
|
||||
# we need to change its destination. Else, the monitor for
|
||||
# `ref.commit` below will fail. In case of writes, we do as before.
|
||||
|
||||
if inp.req.bd.knd = read {
|
||||
assert ~ref.committed(inp.req.tx);
|
||||
assert req_dest(inp.req.tx) = dest.prim;
|
||||
req_dest(inp.req.tx) := dest.sec
|
||||
} else {
|
||||
assert inp.req.tx = queue.pop;
|
||||
};
|
||||
if inp.req.bd.knd = read {
|
||||
assert ~ref.committed(inp.req.tx);
|
||||
assert req_dest(inp.req.tx) = dest.prim;
|
||||
req_dest(inp.req.tx) := dest.sec
|
||||
} else {
|
||||
assert inp.req.tx = queue.pop;
|
||||
};
|
||||
|
||||
call ref.commit(inp.req.tx,dest.sec);
|
||||
call ref.commit(inp.req.tx,dest.sec);
|
||||
}
|
||||
|
||||
# This tells IVy that the above specification is a guarantee for
|
||||
|
|
@ -463,7 +463,7 @@ object mid_spec = {
|
|||
relation acked(X:txid)
|
||||
|
||||
after init {
|
||||
acked(X) := false;
|
||||
acked(X) := false;
|
||||
}
|
||||
|
||||
# When an ack message is sent on the reverse channel, it must have
|
||||
|
|
@ -472,10 +472,10 @@ object mid_spec = {
|
|||
# fact that it is now acked.
|
||||
|
||||
before rev_chan.sndr.send(inp : req_msg) {
|
||||
assert ref.committed(inp.req.tx);
|
||||
assert ref.txs(inp.req.tx) = inp.req.bd;
|
||||
assert ~acked(inp.req.tx);
|
||||
acked(inp.req.tx) := true;
|
||||
assert ref.committed(inp.req.tx);
|
||||
assert ref.txs(inp.req.tx) = inp.req.bd;
|
||||
assert ~acked(inp.req.tx);
|
||||
acked(inp.req.tx) := true;
|
||||
}
|
||||
|
||||
# When a request is created, we record the destination server. In
|
||||
|
|
@ -491,24 +491,24 @@ object mid_spec = {
|
|||
function req_dest(X:txid) : dest.t
|
||||
|
||||
after ref.create(inp : request_body.t, dst:dest.t) returns (tx : txid) {
|
||||
req_dest(tx) := dst
|
||||
req_dest(tx) := dst
|
||||
}
|
||||
|
||||
|
||||
# We now specify that all reads must be commited by the server
|
||||
# they are addressed to, while all writes are committed by the
|
||||
# secondary
|
||||
|
||||
before ref.commit(tx : txid,dst:dest.t) {
|
||||
assert ref.txs(tx).knd = read -> req_dest(tx) = dst;
|
||||
assert ref.txs(tx).knd = write -> dst = dest.sec
|
||||
assert ref.txs(tx).knd = read -> req_dest(tx) = dst;
|
||||
assert ref.txs(tx).knd = write -> dst = dest.sec
|
||||
}
|
||||
|
||||
# Commit immediately all read requests from client to secondary
|
||||
|
||||
before sec.req_chan.recv(inp : req_msg) {
|
||||
if inp.req.bd.knd = read {
|
||||
call ref.commit(inp.req.tx,dest.sec)
|
||||
}
|
||||
if inp.req.bd.knd = read {
|
||||
call ref.commit(inp.req.tx,dest.sec)
|
||||
}
|
||||
}
|
||||
|
||||
}
|
||||
|
|
|
|||
|
|
@ -9,10 +9,7 @@ Project("{8BC9CEB8-8B4A-11D0-8D11-00A0C91BC942}") = "repstore2ex_soln_sec", "rep
|
|||
EndProject
|
||||
Global
|
||||
GlobalSection(SolutionConfigurationPlatforms) = preSolution
|
||||
Debug|x64 = Debug|x64
|
||||
Debug|x86 = Debug|x86
|
||||
Release|x64 = Release|x64
|
||||
Release|x86 = Release|x86
|
||||
EndGlobalSection
|
||||
GlobalSection(ProjectConfigurationPlatforms) = postSolution
|
||||
{A48A9407-CA01-4B56-8D51-303F4FC5F6E1}.Debug|x64.ActiveCfg = Debug|x64
|
||||
|
|
|
|||
|
|
@ -36,29 +36,29 @@ type request_kind = {write,read}
|
|||
|
||||
object request_body = {
|
||||
type t = struct {
|
||||
knd : request_kind,
|
||||
ky : key,
|
||||
vl : value
|
||||
knd : request_kind,
|
||||
ky : key,
|
||||
vl : value
|
||||
}
|
||||
}
|
||||
|
||||
object request = {
|
||||
type t = struct {
|
||||
tx : txid,
|
||||
bd : request_body.t
|
||||
tx : txid,
|
||||
bd : request_body.t
|
||||
}
|
||||
}
|
||||
|
||||
object response_body = {
|
||||
type t = struct {
|
||||
vl : value
|
||||
vl : value
|
||||
}
|
||||
}
|
||||
|
||||
object response = {
|
||||
type t = struct {
|
||||
tx : txid,
|
||||
bd : response_body.t
|
||||
tx : txid,
|
||||
bd : response_body.t
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -67,15 +67,15 @@ object response = {
|
|||
module replica = {
|
||||
function store(K:key) : value
|
||||
after init {
|
||||
store(K) := 0
|
||||
store(K) := 0
|
||||
}
|
||||
action exec(inp : request_body.t) returns (out:response_body.t) = {
|
||||
if inp.knd = write {
|
||||
store(inp.ky) := inp.vl;
|
||||
}
|
||||
else if inp.knd = read {
|
||||
out.vl := store(inp.ky);
|
||||
}
|
||||
if inp.knd = write {
|
||||
store(inp.ky) := inp.vl;
|
||||
}
|
||||
else if inp.knd = read {
|
||||
out.vl := store(inp.ky);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -102,27 +102,27 @@ object ref = {
|
|||
relation committed(X:txid)
|
||||
|
||||
after init {
|
||||
next := 0;
|
||||
committed(X) := false;
|
||||
next := 0;
|
||||
committed(X) := false;
|
||||
}
|
||||
|
||||
implement create {
|
||||
tx := next;
|
||||
txs(tx) := inp;
|
||||
next := next + 1;
|
||||
tx := next;
|
||||
txs(tx) := inp;
|
||||
next := next + 1;
|
||||
}
|
||||
|
||||
implement commit {
|
||||
assert 0 <= tx & tx < next;
|
||||
assert ~committed(tx);
|
||||
txres(tx) := rep.exec(txs(tx));
|
||||
committed(tx) := true;
|
||||
assert 0 <= tx & tx < next;
|
||||
assert ~committed(tx);
|
||||
txres(tx) := rep.exec(txs(tx));
|
||||
committed(tx) := true;
|
||||
}
|
||||
delegate commit
|
||||
|
||||
implement eval {
|
||||
assert committed(tx);
|
||||
res := txres(tx);
|
||||
assert committed(tx);
|
||||
res := txres(tx);
|
||||
}
|
||||
delegate eval
|
||||
|
||||
|
|
@ -142,7 +142,7 @@ object ser = {
|
|||
relation serialized(X:txid)
|
||||
|
||||
after init {
|
||||
serialized(X) := false;
|
||||
serialized(X) := false;
|
||||
}
|
||||
|
||||
# To serialzie a write, we must guarantee that transaction exists,
|
||||
|
|
@ -150,10 +150,10 @@ object ser = {
|
|||
# only serialize write transactions.
|
||||
|
||||
implement serialize {
|
||||
assert 0 <= tx & tx < ref.next;
|
||||
assert ~serialized(tx);
|
||||
assert ref.txs(tx).knd = write;
|
||||
serialized(tx) := true;
|
||||
assert 0 <= tx & tx < ref.next;
|
||||
assert ~serialized(tx);
|
||||
assert ref.txs(tx).knd = write;
|
||||
serialized(tx) := true;
|
||||
}
|
||||
delegate serialize
|
||||
|
||||
|
|
@ -161,7 +161,7 @@ object ser = {
|
|||
# until it is serialized.
|
||||
|
||||
before ref.commit(tx : txid,dst:dest.t) {
|
||||
assert ref.txs(tx).knd = write -> serialized(tx);
|
||||
assert ref.txs(tx).knd = write -> serialized(tx);
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -187,19 +187,19 @@ module client(cid,prim_chan,sec_chan,cl_chans) = {
|
|||
action client_response(req : response_body.t, tx : txid)
|
||||
|
||||
implement client_request {
|
||||
var m : req_msg;
|
||||
m.cid := cid;
|
||||
m.req.tx := ref.create(req,the_dst);
|
||||
m.req.bd := req;
|
||||
if the_dst = dest.prim {
|
||||
call prim_chan.send(m);
|
||||
} else {
|
||||
call sec_chan.send(m);
|
||||
}
|
||||
var m : req_msg;
|
||||
m.cid := cid;
|
||||
m.req.tx := ref.create(req,the_dst);
|
||||
m.req.bd := req;
|
||||
if the_dst = dest.prim {
|
||||
call prim_chan.send(m);
|
||||
} else {
|
||||
call sec_chan.send(m);
|
||||
}
|
||||
}
|
||||
|
||||
implement cl_chans.recv(resp : response.t) {
|
||||
call client_response(resp.bd,resp.tx)
|
||||
call client_response(resp.bd,resp.tx)
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -222,14 +222,14 @@ module primary_node(port, fwd_chan, rev_chan, cl_chans) = {
|
|||
var sec_failed : bool
|
||||
|
||||
after init {
|
||||
pending(K) := 0;
|
||||
sec_failed := false;
|
||||
pending(K) := 0;
|
||||
sec_failed := false;
|
||||
}
|
||||
|
||||
|
||||
# If we receive a failure message, set `sec_failed`.
|
||||
|
||||
implement fail_chan.recv(inp : fail_msg) {
|
||||
sec_failed := true;
|
||||
sec_failed := true;
|
||||
}
|
||||
|
||||
|
||||
|
|
@ -237,35 +237,35 @@ module primary_node(port, fwd_chan, rev_chan, cl_chans) = {
|
|||
# and we no longer wait for acks.
|
||||
|
||||
implement req_chan.recv(inp : req_msg) {
|
||||
var rr := inp.req.bd;
|
||||
var rr := inp.req.bd;
|
||||
if rr.knd = read {
|
||||
if pending(rr.ky) = 0 | sec_failed {
|
||||
call ref.commit(inp.req.tx,dest.prim);
|
||||
var res : response.t;
|
||||
res.tx := inp.req.tx;
|
||||
res.bd := rep.exec(rr);
|
||||
call cl_chans(inp.cid).send(res)
|
||||
} else {
|
||||
if pending(rr.ky) = 0 | sec_failed {
|
||||
call ref.commit(inp.req.tx,dest.prim);
|
||||
var res : response.t;
|
||||
res.tx := inp.req.tx;
|
||||
res.bd := rep.exec(rr);
|
||||
call cl_chans(inp.cid).send(res)
|
||||
} else {
|
||||
call req_chan.send(inp); # if cannot execute, recirculate
|
||||
}
|
||||
} else if rr.knd = write {
|
||||
call ser.serialize(inp.req.tx); # this is ghost!
|
||||
call fwd_chan.send(inp);
|
||||
if ~sec_failed {
|
||||
pending(rr.ky) := pending(rr.ky).next;
|
||||
var res := rep.exec(inp.req.bd);
|
||||
}
|
||||
}
|
||||
}
|
||||
} else if rr.knd = write {
|
||||
call ser.serialize(inp.req.tx); # this is ghost!
|
||||
call fwd_chan.send(inp);
|
||||
if ~sec_failed {
|
||||
pending(rr.ky) := pending(rr.ky).next;
|
||||
var res := rep.exec(inp.req.bd);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
# When we receive a write request on the acknowledgement channel,
|
||||
# we decrement the pending count of the key.
|
||||
|
||||
implement rev_chan.recv(inp : req_msg) {
|
||||
var rr := inp.req.bd;
|
||||
if rr.knd = write {
|
||||
pending(rr.ky) := pending(rr.ky).prev;
|
||||
}
|
||||
var rr := inp.req.bd;
|
||||
if rr.knd = write {
|
||||
pending(rr.ky) := pending(rr.ky).prev;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -276,31 +276,31 @@ module secondary_node(port, fwd_chan, rev_chan, fail_chan, cl_chans) = {
|
|||
instance rep : replica
|
||||
|
||||
instance req_chan : nondup_endpoint(port,req_msg)
|
||||
|
||||
|
||||
var failed : bool
|
||||
|
||||
after init {
|
||||
failed := false;
|
||||
failed := false;
|
||||
}
|
||||
|
||||
action fail = {
|
||||
failed := true;
|
||||
var m : fail_msg;
|
||||
call fail_chan.send(m);
|
||||
failed := true;
|
||||
var m : fail_msg;
|
||||
call fail_chan.send(m);
|
||||
}
|
||||
|
||||
implement req_chan.recv(inp : req_msg) {
|
||||
if ~failed {
|
||||
var rr := inp.req.bd;
|
||||
if rr.knd = read {
|
||||
call ref.commit(inp.req.tx,dest.sec);
|
||||
var res : response.t;
|
||||
res.tx := inp.req.tx;
|
||||
res.bd := rep.exec(rr);
|
||||
call cl_chans(inp.cid).send(res);
|
||||
}
|
||||
# ignore writes!
|
||||
}
|
||||
if ~failed {
|
||||
var rr := inp.req.bd;
|
||||
if rr.knd = read {
|
||||
call ref.commit(inp.req.tx,dest.sec);
|
||||
var res : response.t;
|
||||
res.tx := inp.req.tx;
|
||||
res.bd := rep.exec(rr);
|
||||
call cl_chans(inp.cid).send(res);
|
||||
}
|
||||
# ignore writes!
|
||||
}
|
||||
}
|
||||
|
||||
# When the secondary receives a forwarded write from the primary,
|
||||
|
|
@ -309,13 +309,13 @@ module secondary_node(port, fwd_chan, rev_chan, fail_chan, cl_chans) = {
|
|||
#
|
||||
|
||||
implement fwd_chan.recv(inp : req_msg) {
|
||||
if ~failed {
|
||||
var res : response.t;
|
||||
res.tx := inp.req.tx;
|
||||
res.bd := rep.exec(inp.req.bd);
|
||||
call cl_chans(inp.cid).send(res);
|
||||
call rev_chan.send(inp);
|
||||
}
|
||||
if ~failed {
|
||||
var res : response.t;
|
||||
res.tx := inp.req.tx;
|
||||
res.bd := rep.exec(inp.req.bd);
|
||||
call cl_chans(inp.cid).send(res);
|
||||
call rev_chan.send(inp);
|
||||
}
|
||||
}
|
||||
|
||||
}
|
||||
|
|
@ -351,13 +351,13 @@ object service_spec = {
|
|||
relation responded(X:txid)
|
||||
|
||||
after init {
|
||||
responded(X) := false;
|
||||
responded(X) := false;
|
||||
}
|
||||
|
||||
before cl_chans.send(p : client_id, m : response.t) {
|
||||
assert ~responded(m.tx);
|
||||
assert m.bd = ref.eval(m.tx);
|
||||
responded(m.tx) := true;
|
||||
assert ~responded(m.tx);
|
||||
assert m.bd = ref.eval(m.tx);
|
||||
responded(m.tx) := true;
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -368,9 +368,9 @@ object mid_spec = {
|
|||
instance queue : unbounded_queue(txid)
|
||||
|
||||
before fwd_chan.rcvr.recv(inp : req_msg) {
|
||||
assert inp.req.bd = ref.txs(inp.req.tx);
|
||||
assert inp.req.tx = queue.pop;
|
||||
call ref.commit(inp.req.tx,dest.sec);
|
||||
assert inp.req.bd = ref.txs(inp.req.tx);
|
||||
assert inp.req.tx = queue.pop;
|
||||
call ref.commit(inp.req.tx,dest.sec);
|
||||
}
|
||||
|
||||
delegate fwd_chan_rcvr_recv[before] -> prim
|
||||
|
|
@ -382,37 +382,37 @@ object mid_spec = {
|
|||
var sec_failed : bool
|
||||
|
||||
after init {
|
||||
acked(X) := false;
|
||||
sec_failed := false;
|
||||
acked(X) := false;
|
||||
sec_failed := false;
|
||||
}
|
||||
|
||||
before rev_chan.sndr.send(inp : req_msg) {
|
||||
assert ref.committed(inp.req.tx);
|
||||
assert ref.txs(inp.req.tx) = inp.req.bd;
|
||||
assert ~acked(inp.req.tx);
|
||||
acked(inp.req.tx) := true;
|
||||
assert ref.committed(inp.req.tx);
|
||||
assert ref.txs(inp.req.tx) = inp.req.bd;
|
||||
assert ~acked(inp.req.tx);
|
||||
acked(inp.req.tx) := true;
|
||||
}
|
||||
|
||||
# If the secondary has failed, then write transactions are commited at the
|
||||
# moment they are serialized.
|
||||
|
||||
after ser.serialize(tx:txid) {
|
||||
call queue.push(tx);
|
||||
if sec_failed {
|
||||
call ref.commit(tx)
|
||||
}
|
||||
call queue.push(tx);
|
||||
if sec_failed {
|
||||
call ref.commit(tx)
|
||||
}
|
||||
}
|
||||
|
||||
function req_dest(X:txid) : dest.t
|
||||
|
||||
after ref.create(inp : request_body.t, dst:dest.t) returns (tx : txid) {
|
||||
req_dest(tx) := dst
|
||||
req_dest(tx) := dst
|
||||
}
|
||||
|
||||
|
||||
# Here, we set the `sec_failed` flag.
|
||||
|
||||
after prim.fail_chan.send(m : fail_msg) {
|
||||
sec_failed := true;
|
||||
sec_failed := true;
|
||||
}
|
||||
|
||||
# After a failure of the secondary, the primary is allowed to
|
||||
|
|
@ -420,12 +420,12 @@ object mid_spec = {
|
|||
# anything.
|
||||
|
||||
before ref.commit(tx : txid,dst:dest.t) {
|
||||
assert ref.txs(tx).knd = read -> req_dest(tx) = dst;
|
||||
if sec_failed {
|
||||
assert dst = dst.prim
|
||||
} else {
|
||||
assert ref.txs(tx).knd = write -> dst = dest.sec
|
||||
}
|
||||
assert ref.txs(tx).knd = read -> req_dest(tx) = dst;
|
||||
if sec_failed {
|
||||
assert dst = dst.prim
|
||||
} else {
|
||||
assert ref.txs(tx).knd = write -> dst = dest.sec
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -34,29 +34,29 @@ type request_kind = {write,read}
|
|||
|
||||
object request_body = {
|
||||
type t = struct {
|
||||
knd : request_kind,
|
||||
ky : key,
|
||||
vl : value
|
||||
knd : request_kind,
|
||||
ky : key,
|
||||
vl : value
|
||||
}
|
||||
}
|
||||
|
||||
object request = {
|
||||
type t = struct {
|
||||
tx : txid,
|
||||
bd : request_body.t
|
||||
tx : txid,
|
||||
bd : request_body.t
|
||||
}
|
||||
}
|
||||
|
||||
object response_body = {
|
||||
type t = struct {
|
||||
vl : value
|
||||
vl : value
|
||||
}
|
||||
}
|
||||
|
||||
object response = {
|
||||
type t = struct {
|
||||
tx : txid,
|
||||
bd : response_body.t
|
||||
tx : txid,
|
||||
bd : response_body.t
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -65,15 +65,15 @@ object response = {
|
|||
module replica = {
|
||||
function store(K:key) : value
|
||||
after init {
|
||||
store(K) := 0
|
||||
store(K) := 0
|
||||
}
|
||||
action exec(inp : request_body.t) returns (out:response_body.t) = {
|
||||
if inp.knd = write {
|
||||
store(inp.ky) := inp.vl;
|
||||
}
|
||||
else if inp.knd = read {
|
||||
out.vl := store(inp.ky);
|
||||
}
|
||||
if inp.knd = write {
|
||||
store(inp.ky) := inp.vl;
|
||||
}
|
||||
else if inp.knd = read {
|
||||
out.vl := store(inp.ky);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -100,27 +100,27 @@ object ref = {
|
|||
relation committed(X:txid)
|
||||
|
||||
after init {
|
||||
next := 0;
|
||||
committed(X) := false;
|
||||
next := 0;
|
||||
committed(X) := false;
|
||||
}
|
||||
|
||||
implement create {
|
||||
tx := next;
|
||||
txs(tx) := inp;
|
||||
next := next + 1;
|
||||
tx := next;
|
||||
txs(tx) := inp;
|
||||
next := next + 1;
|
||||
}
|
||||
|
||||
implement commit {
|
||||
assert 0 <= tx & tx < next;
|
||||
assert ~committed(tx);
|
||||
txres(tx) := rep.exec(txs(tx));
|
||||
committed(tx) := true;
|
||||
assert 0 <= tx & tx < next;
|
||||
assert ~committed(tx);
|
||||
txres(tx) := rep.exec(txs(tx));
|
||||
committed(tx) := true;
|
||||
}
|
||||
delegate commit
|
||||
|
||||
implement eval {
|
||||
assert committed(tx);
|
||||
res := txres(tx);
|
||||
assert committed(tx);
|
||||
res := txres(tx);
|
||||
}
|
||||
delegate eval
|
||||
|
||||
|
|
@ -140,7 +140,7 @@ object ser = {
|
|||
relation serialized(X:txid)
|
||||
|
||||
after init {
|
||||
serialized(X) := false;
|
||||
serialized(X) := false;
|
||||
}
|
||||
|
||||
# To serialzie a write, we must guarantee that transaction exists,
|
||||
|
|
@ -148,10 +148,10 @@ object ser = {
|
|||
# only serialize write transactions.
|
||||
|
||||
implement serialize {
|
||||
assert 0 <= tx & tx < ref.next;
|
||||
assert ~serialized(tx);
|
||||
assert ref.txs(tx).knd = write;
|
||||
serialized(tx) := true;
|
||||
assert 0 <= tx & tx < ref.next;
|
||||
assert ~serialized(tx);
|
||||
assert ref.txs(tx).knd = write;
|
||||
serialized(tx) := true;
|
||||
}
|
||||
delegate serialize
|
||||
|
||||
|
|
@ -159,7 +159,7 @@ object ser = {
|
|||
# until it is serialized.
|
||||
|
||||
before ref.commit(tx : txid,dst:dest.t) {
|
||||
assert ref.txs(tx).knd = write -> serialized(tx);
|
||||
assert ref.txs(tx).knd = write -> serialized(tx);
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -176,8 +176,8 @@ type client_id
|
|||
|
||||
object req_msg = {
|
||||
type t = struct {
|
||||
cid : client_id,
|
||||
req : request.t
|
||||
cid : client_id,
|
||||
req : request.t
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -187,19 +187,19 @@ module client(cid,prim_chan,sec_chan,cl_chans) = {
|
|||
action client_response(resp : response_body.t, tx : txid)
|
||||
|
||||
implement client_request {
|
||||
var m : req_msg.t;
|
||||
m.cid := cid;
|
||||
m.req.tx := ref.create(the_req,the_dst);
|
||||
m.req.bd := the_req;
|
||||
if the_dst = dest.prim {
|
||||
call prim_chan.send(m);
|
||||
} else {
|
||||
call sec_chan.send(m);
|
||||
}
|
||||
var m : req_msg.t;
|
||||
m.cid := cid;
|
||||
m.req.tx := ref.create(the_req,the_dst);
|
||||
m.req.bd := the_req;
|
||||
if the_dst = dest.prim {
|
||||
call prim_chan.send(m);
|
||||
} else {
|
||||
call sec_chan.send(m);
|
||||
}
|
||||
}
|
||||
|
||||
implement cl_chans.recv(resp : response.t) {
|
||||
call client_response(resp.bd,resp.tx)
|
||||
call client_response(resp.bd,resp.tx)
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -222,14 +222,14 @@ module primary_node(port, fwd_chan, rev_chan, cl_chans) = {
|
|||
var sec_failed : bool
|
||||
|
||||
after init {
|
||||
pending(K) := 0;
|
||||
sec_failed := false;
|
||||
pending(K) := 0;
|
||||
sec_failed := false;
|
||||
}
|
||||
|
||||
|
||||
# If we receive a failure message, set `sec_failed`.
|
||||
|
||||
implement fail_chan.recv(inp : fail_msg) {
|
||||
sec_failed := true;
|
||||
sec_failed := true;
|
||||
}
|
||||
|
||||
|
||||
|
|
@ -237,35 +237,35 @@ module primary_node(port, fwd_chan, rev_chan, cl_chans) = {
|
|||
# and we no longer wait for acks.
|
||||
|
||||
implement req_chan.recv(inp : req_msg.t) {
|
||||
var rr := inp.req.bd;
|
||||
var rr := inp.req.bd;
|
||||
if rr.knd = read {
|
||||
if pending(rr.ky) = 0 | sec_failed {
|
||||
call ref.commit(inp.req.tx,dest.prim);
|
||||
var res : response.t;
|
||||
res.tx := inp.req.tx;
|
||||
res.bd := rep.exec(rr);
|
||||
call cl_chans(inp.cid).send(res)
|
||||
} else {
|
||||
if pending(rr.ky) = 0 | sec_failed {
|
||||
call ref.commit(inp.req.tx,dest.prim);
|
||||
var res : response.t;
|
||||
res.tx := inp.req.tx;
|
||||
res.bd := rep.exec(rr);
|
||||
call cl_chans(inp.cid).send(res)
|
||||
} else {
|
||||
call req_chan.send(inp); # if cannot execute, recirculate
|
||||
}
|
||||
} else if rr.knd = write {
|
||||
call ser.serialize(inp.req.tx); # this is ghost!
|
||||
if ~sec_failed {
|
||||
call fwd_chan.send(inp);
|
||||
pending(rr.ky) := pending(rr.ky).next;
|
||||
};
|
||||
var res := rep.exec(inp.req.bd);
|
||||
}
|
||||
}
|
||||
} else if rr.knd = write {
|
||||
call ser.serialize(inp.req.tx); # this is ghost!
|
||||
if ~sec_failed {
|
||||
call fwd_chan.send(inp);
|
||||
pending(rr.ky) := pending(rr.ky).next;
|
||||
};
|
||||
var res := rep.exec(inp.req.bd);
|
||||
}
|
||||
}
|
||||
|
||||
# When we receive a write request on the acknowledgement channel,
|
||||
# we decrement the pending count of the key.
|
||||
|
||||
implement rev_chan.recv(inp : req_msg.t) {
|
||||
var rr := inp.req.bd;
|
||||
if rr.knd = write {
|
||||
pending(rr.ky) := pending(rr.ky).prev;
|
||||
}
|
||||
var rr := inp.req.bd;
|
||||
if rr.knd = write {
|
||||
pending(rr.ky) := pending(rr.ky).prev;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -276,33 +276,33 @@ module secondary_node(port, fwd_chan, rev_chan, fail_chan, cl_chans) = {
|
|||
instance rep : replica
|
||||
|
||||
instance req_chan : nondup_endpoint(port,req_msg.t)
|
||||
|
||||
|
||||
var failed : bool
|
||||
|
||||
after init {
|
||||
failed := false;
|
||||
failed := false;
|
||||
}
|
||||
|
||||
action fail = {
|
||||
if ~failed {
|
||||
failed := true;
|
||||
var m : fail_msg;
|
||||
call fail_chan.send(m);
|
||||
}
|
||||
if ~failed {
|
||||
failed := true;
|
||||
var m : fail_msg;
|
||||
call fail_chan.send(m);
|
||||
}
|
||||
}
|
||||
|
||||
implement req_chan.recv(inp : req_msg.t) {
|
||||
if ~failed {
|
||||
var rr := inp.req.bd;
|
||||
if rr.knd = read {
|
||||
call ref.commit(inp.req.tx,dest.sec);
|
||||
var res : response.t;
|
||||
res.tx := inp.req.tx;
|
||||
res.bd := rep.exec(rr);
|
||||
call cl_chans(inp.cid).send(res);
|
||||
}
|
||||
# ignore writes!
|
||||
}
|
||||
if ~failed {
|
||||
var rr := inp.req.bd;
|
||||
if rr.knd = read {
|
||||
call ref.commit(inp.req.tx,dest.sec);
|
||||
var res : response.t;
|
||||
res.tx := inp.req.tx;
|
||||
res.bd := rep.exec(rr);
|
||||
call cl_chans(inp.cid).send(res);
|
||||
}
|
||||
# ignore writes!
|
||||
}
|
||||
}
|
||||
|
||||
# When the secondary receives a forwarded write from the primary,
|
||||
|
|
@ -311,13 +311,13 @@ module secondary_node(port, fwd_chan, rev_chan, fail_chan, cl_chans) = {
|
|||
#
|
||||
|
||||
implement fwd_chan.recv(inp : req_msg.t) {
|
||||
if ~failed {
|
||||
var res : response.t;
|
||||
res.tx := inp.req.tx;
|
||||
res.bd := rep.exec(inp.req.bd);
|
||||
call cl_chans(inp.cid).send(res);
|
||||
call rev_chan.send(inp);
|
||||
}
|
||||
if ~failed {
|
||||
var res : response.t;
|
||||
res.tx := inp.req.tx;
|
||||
res.bd := rep.exec(inp.req.bd);
|
||||
call cl_chans(inp.cid).send(res);
|
||||
call rev_chan.send(inp);
|
||||
}
|
||||
}
|
||||
|
||||
}
|
||||
|
|
@ -353,13 +353,13 @@ object service_spec = {
|
|||
relation responded(X:txid)
|
||||
|
||||
after init {
|
||||
responded(X) := false;
|
||||
responded(X) := false;
|
||||
}
|
||||
|
||||
before cl_chans.send(p : client_id, m : response.t) {
|
||||
assert ~responded(m.tx);
|
||||
assert m.bd = ref.eval(m.tx);
|
||||
responded(m.tx) := true;
|
||||
assert ~responded(m.tx);
|
||||
assert m.bd = ref.eval(m.tx);
|
||||
responded(m.tx) := true;
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -370,13 +370,13 @@ object mid_spec = {
|
|||
instance queue : unbounded_queue(txid)
|
||||
|
||||
after ser.serialize(tx:txid) {
|
||||
call queue.push(tx);
|
||||
call queue.push(tx);
|
||||
}
|
||||
|
||||
before fwd_chan.rcvr.recv(inp : req_msg.t) {
|
||||
assert inp.req.bd = ref.txs(inp.req.tx);
|
||||
assert inp.req.tx = queue.pop;
|
||||
call ref.commit(inp.req.tx,dest.sec);
|
||||
assert inp.req.bd = ref.txs(inp.req.tx);
|
||||
assert inp.req.tx = queue.pop;
|
||||
call ref.commit(inp.req.tx,dest.sec);
|
||||
}
|
||||
|
||||
delegate fwd_chan_rcvr_recv[before] -> prim
|
||||
|
|
@ -388,32 +388,32 @@ object mid_spec = {
|
|||
var sec_failed : bool
|
||||
|
||||
after init {
|
||||
acked(X) := false;
|
||||
sec_failed := false;
|
||||
acked(X) := false;
|
||||
sec_failed := false;
|
||||
}
|
||||
|
||||
before rev_chan.sndr.send(inp : req_msg.t) {
|
||||
assert ref.committed(inp.req.tx);
|
||||
assert ref.txs(inp.req.tx) = inp.req.bd;
|
||||
assert ~acked(inp.req.tx);
|
||||
assert ~sec_failed;
|
||||
acked(inp.req.tx) := true;
|
||||
assert ref.committed(inp.req.tx);
|
||||
assert ref.txs(inp.req.tx) = inp.req.bd;
|
||||
assert ~acked(inp.req.tx);
|
||||
assert ~sec_failed;
|
||||
acked(inp.req.tx) := true;
|
||||
}
|
||||
|
||||
function req_dest(X:txid) : dest.t
|
||||
|
||||
after ref.create(inp : request_body.t, dst:dest.t) returns (tx : txid) {
|
||||
req_dest(tx) := dst
|
||||
req_dest(tx) := dst
|
||||
}
|
||||
|
||||
|
||||
before prim.fail_chan.send(m : fail_msg) {
|
||||
assert ~sec_failed;
|
||||
assert ~sec_failed;
|
||||
}
|
||||
|
||||
# Here, we set the `sec_failed` flag.
|
||||
|
||||
after prim.fail_chan.send(m : fail_msg) {
|
||||
sec_failed := true;
|
||||
sec_failed := true;
|
||||
}
|
||||
|
||||
# After a failure of the secondary, the primary is allowed to
|
||||
|
|
@ -421,43 +421,43 @@ object mid_spec = {
|
|||
# anything.
|
||||
|
||||
before ref.commit(tx : txid,dst:dest.t) {
|
||||
assert ref.txs(tx).knd = read -> req_dest(tx) = dst;
|
||||
if sec_failed {
|
||||
assert dst = dst.prim
|
||||
} else {
|
||||
assert ref.txs(tx).knd = write -> dst = dest.sec
|
||||
}
|
||||
assert ref.txs(tx).knd = read -> req_dest(tx) = dst;
|
||||
if sec_failed {
|
||||
assert dst = dst.prim
|
||||
} else {
|
||||
assert ref.txs(tx).knd = write -> dst = dest.sec
|
||||
}
|
||||
}
|
||||
|
||||
object solution = {
|
||||
|
||||
# Exercise solution: We maintain an ordered queue of all the
|
||||
# write requests that have been serialized but not commited.
|
||||
|
||||
# Exercise solution: We maintain an ordered queue of all the
|
||||
# write requests that have been serialized but not commited.
|
||||
|
||||
instance pending : unbounded_queue(txid)
|
||||
instance pending : unbounded_queue(txid)
|
||||
|
||||
after ser.serialize(tx:txid) {
|
||||
call pending.push(tx);
|
||||
if sec_failed {
|
||||
call ref.commit(tx,dest.prim)
|
||||
}
|
||||
}
|
||||
after ser.serialize(tx:txid) {
|
||||
call pending.push(tx);
|
||||
if sec_failed {
|
||||
call ref.commit(tx,dest.prim)
|
||||
}
|
||||
}
|
||||
|
||||
after ref.commit(tx : txid,dst:dest.t) {
|
||||
if ref.txs(tx).knd = write {
|
||||
var tmp := pending.pop;
|
||||
}
|
||||
}
|
||||
after ref.commit(tx : txid,dst:dest.t) {
|
||||
if ref.txs(tx).knd = write {
|
||||
var tmp := pending.pop;
|
||||
}
|
||||
}
|
||||
|
||||
# When the secondary says it has failed, we commit all of the
|
||||
# pending write requests.
|
||||
# When the secondary says it has failed, we commit all of the
|
||||
# pending write requests.
|
||||
|
||||
after prim.fail_chan.send(m : fail_msg) {
|
||||
while ~pending.empty {
|
||||
call ref.commit(pending.first,dest.prim)
|
||||
}
|
||||
}
|
||||
}
|
||||
after prim.fail_chan.send(m : fail_msg) {
|
||||
while ~pending.empty {
|
||||
call ref.commit(pending.first,dest.prim)
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
# We export/import our API.
|
||||
|
|
|
|||
|
|
@ -11,21 +11,21 @@ type request_body
|
|||
|
||||
object write_req = {
|
||||
variant t of request_body = struct {
|
||||
ky : key,
|
||||
vl : value
|
||||
ky : key,
|
||||
vl : value
|
||||
}
|
||||
}
|
||||
|
||||
object read_req = {
|
||||
variant t of request_body = struct {
|
||||
ky : key
|
||||
ky : key
|
||||
}
|
||||
}
|
||||
|
||||
object request = {
|
||||
type t = struct {
|
||||
tx : txid,
|
||||
bd : request_body
|
||||
tx : txid,
|
||||
bd : request_body
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -38,33 +38,33 @@ object write_resp = {
|
|||
|
||||
object read_resp = {
|
||||
variant t of response_body = struct {
|
||||
vl : value
|
||||
vl : value
|
||||
}
|
||||
}
|
||||
|
||||
object response = {
|
||||
type t = struct {
|
||||
tx : txid,
|
||||
bd : response_body
|
||||
tx : txid,
|
||||
bd : response_body
|
||||
}
|
||||
}
|
||||
|
||||
module replica = {
|
||||
function store(K:key) : value
|
||||
after init {
|
||||
store(K) := 0
|
||||
store(K) := 0
|
||||
}
|
||||
action exec(inp : request_body) returns (out:response_body) = {
|
||||
if some (r:write_req.t) inp *> r {
|
||||
store(r.ky) := r.vl;
|
||||
var wr : write_resp.t;
|
||||
out := wr
|
||||
}
|
||||
else if some (r:read_req.t) inp *> r {
|
||||
var rr : read_resp.t;
|
||||
rr.vl := store(r.ky);
|
||||
out := rr
|
||||
}
|
||||
if some (r:write_req.t) inp *> r {
|
||||
store(r.ky) := r.vl;
|
||||
var wr : write_resp.t;
|
||||
out := wr
|
||||
}
|
||||
else if some (r:read_req.t) inp *> r {
|
||||
var rr : read_resp.t;
|
||||
rr.vl := store(r.ky);
|
||||
out := rr
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -85,35 +85,35 @@ module reference = {
|
|||
relation committed(X:txid)
|
||||
|
||||
after init {
|
||||
next := 0;
|
||||
committed(X) := false;
|
||||
serialized(X) := false;
|
||||
next := 0;
|
||||
committed(X) := false;
|
||||
serialized(X) := false;
|
||||
}
|
||||
|
||||
implement create {
|
||||
tx := next;
|
||||
txs(tx) := inp;
|
||||
next := next + 1;
|
||||
tx := next;
|
||||
txs(tx) := inp;
|
||||
next := next + 1;
|
||||
}
|
||||
|
||||
implement serialize {
|
||||
assert 0 <= tx & tx < next;
|
||||
assert ~serialized(tx);
|
||||
serialized(tx) := true;
|
||||
assert 0 <= tx & tx < next;
|
||||
assert ~serialized(tx);
|
||||
serialized(tx) := true;
|
||||
}
|
||||
delegate serialize
|
||||
|
||||
implement commit {
|
||||
assert 0 <= tx & tx < next;
|
||||
assert serialized(tx) & ~committed(tx);
|
||||
txres(tx) := rep.exec(txs(tx));
|
||||
committed(tx) := true;
|
||||
assert 0 <= tx & tx < next;
|
||||
assert serialized(tx) & ~committed(tx);
|
||||
txres(tx) := rep.exec(txs(tx));
|
||||
committed(tx) := true;
|
||||
}
|
||||
delegate commit
|
||||
|
||||
implement eval {
|
||||
assert committed(tx);
|
||||
res := txres(tx);
|
||||
assert committed(tx);
|
||||
res := txres(tx);
|
||||
}
|
||||
delegate eval
|
||||
|
||||
|
|
@ -134,11 +134,11 @@ module client(cid,srvr_chan,cl_chans) = {
|
|||
action client_request(req : request_body)
|
||||
|
||||
implement client_request {
|
||||
var m : req_msg;
|
||||
m.cid := cid;
|
||||
m.req.tx := ref.create(req);
|
||||
m.req.bd := req;
|
||||
call srvr_chan.send(m);
|
||||
var m : req_msg;
|
||||
m.cid := cid;
|
||||
m.req.tx := ref.create(req);
|
||||
m.req.bd := req;
|
||||
call srvr_chan.send(m);
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -151,32 +151,32 @@ module primary_node(port, fwd_chan, rev_chan, cl_chans) = {
|
|||
function pending(K:key) : counter.t
|
||||
|
||||
after init {
|
||||
pending(K) := 0;
|
||||
pending(K) := 0;
|
||||
}
|
||||
|
||||
|
||||
implement req_chan.recv(inp : req_msg) {
|
||||
if some (rr:read_req.t) inp.req.bd *> rr {
|
||||
if pending(rr.ky) = 0 {
|
||||
call ref.commit(inp.req.tx);
|
||||
var res : response.t;
|
||||
res.tx := inp.req.tx;
|
||||
res.bd := rep.exec(rr);
|
||||
call cl_chans(inp.cid).send(res)
|
||||
} else {
|
||||
if pending(rr.ky) = 0 {
|
||||
call ref.commit(inp.req.tx);
|
||||
var res : response.t;
|
||||
res.tx := inp.req.tx;
|
||||
res.bd := rep.exec(rr);
|
||||
call cl_chans(inp.cid).send(res)
|
||||
} else {
|
||||
call req_chan.send(inp); # if cannot execute, recirculate
|
||||
}
|
||||
} else if some (wr:write_req.t) inp.req.bd *> wr {
|
||||
call ref.serialize(inp.req.tx); # this is ghost!
|
||||
call fwd_chan.send(inp);
|
||||
pending(wr.ky) := pending(wr.ky).next;
|
||||
var res := rep.exec(inp.req.bd);
|
||||
}
|
||||
}
|
||||
} else if some (wr:write_req.t) inp.req.bd *> wr {
|
||||
call ref.serialize(inp.req.tx); # this is ghost!
|
||||
call fwd_chan.send(inp);
|
||||
pending(wr.ky) := pending(wr.ky).next;
|
||||
var res := rep.exec(inp.req.bd);
|
||||
}
|
||||
}
|
||||
|
||||
implement rev_chan.recv(inp : req_msg) {
|
||||
if some (wr:write_req.t) inp.req.bd *> wr {
|
||||
pending(wr.ky) := pending(wr.ky).prev;
|
||||
}
|
||||
if some (wr:write_req.t) inp.req.bd *> wr {
|
||||
pending(wr.ky) := pending(wr.ky).prev;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -184,24 +184,24 @@ module secondary_node(port, fwd_chan, rev_chan, cl_chans) = {
|
|||
instance rep : replica
|
||||
|
||||
instance req_chan : nondup_endpoint(port,req_msg)
|
||||
|
||||
|
||||
implement req_chan.recv(inp : req_msg) {
|
||||
if some (rr:read_req.t) inp.req.bd *> rr {
|
||||
var res : response.t;
|
||||
res.tx := inp.req.tx;
|
||||
res.bd := rep.exec(rr);
|
||||
call cl_chans(inp.cid).send(res);
|
||||
}
|
||||
# ignore writes!
|
||||
var res : response.t;
|
||||
res.tx := inp.req.tx;
|
||||
res.bd := rep.exec(rr);
|
||||
call cl_chans(inp.cid).send(res);
|
||||
}
|
||||
# ignore writes!
|
||||
}
|
||||
|
||||
implement fwd_chan.recv(inp : req_msg) {
|
||||
call ref.commit(inp.req.tx);
|
||||
var res : response.t;
|
||||
res.tx := inp.req.tx;
|
||||
res.bd := rep.exec(inp.req.bd);
|
||||
call cl_chans(inp.cid).send(res);
|
||||
call rev_chan.send(inp);
|
||||
call ref.commit(inp.req.tx);
|
||||
var res : response.t;
|
||||
res.tx := inp.req.tx;
|
||||
res.bd := rep.exec(inp.req.bd);
|
||||
call cl_chans(inp.cid).send(res);
|
||||
call rev_chan.send(inp);
|
||||
}
|
||||
|
||||
}
|
||||
|
|
@ -217,7 +217,7 @@ instance sec : secondary_node(44201,fwd_chan.rcvr,rev_chan.sndr,cl_chans)
|
|||
|
||||
object service_spec = {
|
||||
before cl_chans.send(p : client_id, m : response.t) {
|
||||
assert m.bd = ref.eval(m.tx);
|
||||
assert m.bd = ref.eval(m.tx);
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -225,13 +225,13 @@ object mid_spec = {
|
|||
instance queue : unbounded_queue(txid)
|
||||
|
||||
after ref.serialize(tx:txid) {
|
||||
call queue.push(tx);
|
||||
call queue.push(tx);
|
||||
}
|
||||
|
||||
before fwd_chan.rcvr.recv(inp : req_msg) {
|
||||
assert inp.req.bd = ref.txs(inp.req.tx);
|
||||
assert inp.req.tx = queue.pop;
|
||||
call ref.commit(inp.req.tx);
|
||||
assert inp.req.bd = ref.txs(inp.req.tx);
|
||||
assert inp.req.tx = queue.pop;
|
||||
call ref.commit(inp.req.tx);
|
||||
}
|
||||
|
||||
delegate fwd_chan_rcvr_recv[before] -> prim
|
||||
|
|
|
|||
|
|
@ -12,7 +12,7 @@ module sequence_numbers = {
|
|||
|
||||
interpret t->bv[8]
|
||||
implement next {
|
||||
res := seq + 1
|
||||
res := seq + 1
|
||||
}
|
||||
|
||||
}
|
||||
|
|
|
|||
|
|
@ -19,7 +19,7 @@ object node = {
|
|||
interpret t -> bv[1]
|
||||
|
||||
action next(x:t) returns (y:t) = {
|
||||
y := x + 1
|
||||
y := x + 1
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -58,18 +58,18 @@ object serv = {
|
|||
action release(v:node.t) # client releases lock
|
||||
|
||||
object spec = {
|
||||
relation lock(X:node.t)
|
||||
init lock(X) <-> X = 0
|
||||
|
||||
before grant {
|
||||
assert ~lock(X);
|
||||
lock(v) := true
|
||||
}
|
||||
|
||||
before release {
|
||||
assert lock(v);
|
||||
lock(v) := false
|
||||
}
|
||||
relation lock(X:node.t)
|
||||
init lock(X) <-> X = 0
|
||||
|
||||
before grant {
|
||||
assert ~lock(X);
|
||||
lock(v) := true
|
||||
}
|
||||
|
||||
before release {
|
||||
assert lock(v);
|
||||
lock(v) := false
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -83,20 +83,20 @@ object proto(me:node.t) = {
|
|||
|
||||
relation token
|
||||
after init {
|
||||
token := me = 0
|
||||
token := me = 0
|
||||
}
|
||||
|
||||
implement serv.release {
|
||||
if token {
|
||||
token := false;
|
||||
var pkt : packet.t;
|
||||
call trans.send(me,node.next(me),pkt)
|
||||
}
|
||||
if token {
|
||||
token := false;
|
||||
var pkt : packet.t;
|
||||
call trans.send(me,node.next(me),pkt)
|
||||
}
|
||||
}
|
||||
|
||||
implement trans.recv(pkt:packet.t) {
|
||||
token := true;
|
||||
call serv.grant(me)
|
||||
token := true;
|
||||
call serv.grant(me)
|
||||
}
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -9,10 +9,7 @@ Project("{8BC9CEB8-8B4A-11D0-8D11-00A0C91BC942}") = "token_ring_trans", "token_r
|
|||
EndProject
|
||||
Global
|
||||
GlobalSection(SolutionConfigurationPlatforms) = preSolution
|
||||
Debug|x64 = Debug|x64
|
||||
Debug|x86 = Debug|x86
|
||||
Release|x64 = Release|x64
|
||||
Release|x86 = Release|x86
|
||||
EndGlobalSection
|
||||
GlobalSection(ProjectConfigurationPlatforms) = postSolution
|
||||
{A48A9407-CA01-4B56-8D51-303F4FC5F6E1}.Debug|x64.ActiveCfg = Debug|x64
|
||||
|
|
|
|||
|
|
@ -50,7 +50,7 @@ object node = {
|
|||
interpret t -> bv[1]
|
||||
|
||||
action next(x:t) returns (y:t) = {
|
||||
y := x + 1
|
||||
y := x + 1
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -75,19 +75,19 @@ module transport(lower,packet,id) = {
|
|||
|
||||
object spec = {
|
||||
|
||||
after init {
|
||||
sent(D,P) := false
|
||||
}
|
||||
after init {
|
||||
sent(D,P) := false
|
||||
}
|
||||
|
||||
before send {
|
||||
assert ~sent(dst,pkt);
|
||||
sent(dst,pkt) := true
|
||||
}
|
||||
before send {
|
||||
assert ~sent(dst,pkt);
|
||||
sent(dst,pkt) := true
|
||||
}
|
||||
|
||||
before recv {
|
||||
assert sent(dst,pkt);
|
||||
sent(dst,pkt) := false
|
||||
}
|
||||
before recv {
|
||||
assert sent(dst,pkt);
|
||||
sent(dst,pkt) := false
|
||||
}
|
||||
}
|
||||
|
||||
instance seq_num : sequence_numbers
|
||||
|
|
@ -97,79 +97,79 @@ module transport(lower,packet,id) = {
|
|||
type mtype = {msg_t, ack_t}
|
||||
|
||||
object net_msg = {
|
||||
type t = struct {
|
||||
mty : mtype,
|
||||
src : id,
|
||||
num : seq_num.t,
|
||||
payload : packet
|
||||
}
|
||||
type t = struct {
|
||||
mty : mtype,
|
||||
src : id,
|
||||
num : seq_num.t,
|
||||
payload : packet
|
||||
}
|
||||
}
|
||||
|
||||
object impl(me:id) = {
|
||||
|
||||
|
||||
|
||||
# Create one outgoing message queue for each host
|
||||
# and a timout for each queue.
|
||||
# Create one outgoing message queue for each host
|
||||
# and a timout for each queue.
|
||||
|
||||
instance mq(D:id) : message_queue(net_msg,seq_num)
|
||||
instance timer(D:id) : timeout_sec
|
||||
instance mq(D:id) : message_queue(net_msg,seq_num)
|
||||
instance timer(D:id) : timeout_sec
|
||||
|
||||
# Keep track of the latest sequence number sent and received
|
||||
# on each channel.
|
||||
# Keep track of the latest sequence number sent and received
|
||||
# on each channel.
|
||||
|
||||
var send_seq(S:id) : seq_num.t
|
||||
var recv_seq(S:id) : seq_num.t
|
||||
var send_seq(S:id) : seq_num.t
|
||||
var recv_seq(S:id) : seq_num.t
|
||||
|
||||
init recv_seq(S) = 0 & send_seq(S) = 0
|
||||
init recv_seq(S) = 0 & send_seq(S) = 0
|
||||
|
||||
# Implementations of interface actions
|
||||
# Implementations of interface actions
|
||||
|
||||
implement send(dst:id,pkt:packet) {
|
||||
var msg : net_msg.t;
|
||||
var seq : seq_num.t;
|
||||
msg.mty := msg_t;
|
||||
msg.src := me;
|
||||
msg.num := send_seq(dst);
|
||||
msg.payload := pkt;
|
||||
send_seq(dst) := send_seq(dst).next;
|
||||
call mq(dst).enqueue(msg);
|
||||
call lower.send(me,dst,msg)
|
||||
}
|
||||
implement send(dst:id,pkt:packet) {
|
||||
var msg : net_msg.t;
|
||||
var seq : seq_num.t;
|
||||
msg.mty := msg_t;
|
||||
msg.src := me;
|
||||
msg.num := send_seq(dst);
|
||||
msg.payload := pkt;
|
||||
send_seq(dst) := send_seq(dst).next;
|
||||
call mq(dst).enqueue(msg);
|
||||
call lower.send(me,dst,msg)
|
||||
}
|
||||
|
||||
# Receiving a message is the most complicated. First, we send
|
||||
# an ack. Then, if the sequence number is correct, we call the
|
||||
# application layer action determined by the message type.
|
||||
# Receiving a message is the most complicated. First, we send
|
||||
# an ack. Then, if the sequence number is correct, we call the
|
||||
# application layer action determined by the message type.
|
||||
|
||||
implement lower.recv(msg:net_msg.t) {
|
||||
var src:id;
|
||||
var seq:seq_num.t;
|
||||
seq := msg.num;
|
||||
src := msg.src;
|
||||
if seq <= recv_seq(src) & msg.mty ~= ack_t {
|
||||
var ack : net_msg.t;
|
||||
ack.mty := ack_t;
|
||||
ack.src := me;
|
||||
ack.num := seq;
|
||||
call lower.send(me,src,ack)
|
||||
};
|
||||
if msg.mty = ack_t {
|
||||
call mq(src).delete_all(seq)
|
||||
}
|
||||
else if seq >= recv_seq(src) {
|
||||
recv_seq(src) := seq_num.next(recv_seq(src));
|
||||
call recv(me,msg.payload)
|
||||
}
|
||||
}
|
||||
implement lower.recv(msg:net_msg.t) {
|
||||
var src:id;
|
||||
var seq:seq_num.t;
|
||||
seq := msg.num;
|
||||
src := msg.src;
|
||||
if seq <= recv_seq(src) & msg.mty ~= ack_t {
|
||||
var ack : net_msg.t;
|
||||
ack.mty := ack_t;
|
||||
ack.src := me;
|
||||
ack.num := seq;
|
||||
call lower.send(me,src,ack)
|
||||
};
|
||||
if msg.mty = ack_t {
|
||||
call mq(src).delete_all(seq)
|
||||
}
|
||||
else if seq >= recv_seq(src) {
|
||||
recv_seq(src) := seq_num.next(recv_seq(src));
|
||||
call recv(me,msg.payload)
|
||||
}
|
||||
}
|
||||
|
||||
# If an outgoing channel times out and the queue is not empty,
|
||||
# we pick an arbitrary message in the queue and retransmit it.
|
||||
# If an outgoing channel times out and the queue is not empty,
|
||||
# we pick an arbitrary message in the queue and retransmit it.
|
||||
|
||||
implement timer.timeout(dst:id) {
|
||||
if ~mq(dst).empty {
|
||||
call lower.send(me,dst,mq(dst).pick_one)
|
||||
}
|
||||
}
|
||||
implement timer.timeout(dst:id) {
|
||||
if ~mq(dst).empty {
|
||||
call lower.send(me,dst,mq(dst).pick_one)
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
}
|
||||
|
|
@ -202,18 +202,18 @@ object serv = {
|
|||
action release(v:node.t) # client releases lock
|
||||
|
||||
object spec = {
|
||||
relation lock(X:node.t)
|
||||
init lock(X) <-> X = 0
|
||||
|
||||
before grant {
|
||||
assert ~lock(X);
|
||||
lock(v) := true
|
||||
}
|
||||
|
||||
before release {
|
||||
assert lock(v);
|
||||
lock(v) := false
|
||||
}
|
||||
relation lock(X:node.t)
|
||||
init lock(X) <-> X = 0
|
||||
|
||||
before grant {
|
||||
assert ~lock(X);
|
||||
lock(v) := true
|
||||
}
|
||||
|
||||
before release {
|
||||
assert lock(v);
|
||||
lock(v) := false
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -227,20 +227,20 @@ object proto(me:node.t) = {
|
|||
|
||||
relation token
|
||||
after init {
|
||||
token := me = 0
|
||||
token := me = 0
|
||||
}
|
||||
|
||||
implement serv.release {
|
||||
if token {
|
||||
token := false;
|
||||
var pkt : packet.t;
|
||||
call trans.send(me,node.next(me),pkt)
|
||||
}
|
||||
if token {
|
||||
token := false;
|
||||
var pkt : packet.t;
|
||||
call trans.send(me,node.next(me),pkt)
|
||||
}
|
||||
}
|
||||
|
||||
implement trans.recv(pkt:packet.t) {
|
||||
token := true;
|
||||
call serv.grant(me)
|
||||
token := true;
|
||||
call serv.grant(me)
|
||||
}
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -9,10 +9,7 @@ Project("{8BC9CEB8-8B4A-11D0-8D11-00A0C91BC942}") = "token_ring_buggy_trans", "t
|
|||
EndProject
|
||||
Global
|
||||
GlobalSection(SolutionConfigurationPlatforms) = preSolution
|
||||
Debug|x64 = Debug|x64
|
||||
Debug|x86 = Debug|x86
|
||||
Release|x64 = Release|x64
|
||||
Release|x86 = Release|x86
|
||||
EndGlobalSection
|
||||
GlobalSection(ProjectConfigurationPlatforms) = postSolution
|
||||
{A48A9407-CA01-4B56-8D51-303F4FC5F6E1}.Debug|x64.ActiveCfg = Debug|x64
|
||||
|
|
|
|||
|
|
@ -13,19 +13,19 @@ module transport(lower,packet,id) = {
|
|||
|
||||
object spec = {
|
||||
|
||||
after init {
|
||||
sent(D,P) := false
|
||||
}
|
||||
after init {
|
||||
sent(D,P) := false
|
||||
}
|
||||
|
||||
before send {
|
||||
assert ~sent(dst,pkt);
|
||||
sent(dst,pkt) := true
|
||||
}
|
||||
before send {
|
||||
assert ~sent(dst,pkt);
|
||||
sent(dst,pkt) := true
|
||||
}
|
||||
|
||||
before recv {
|
||||
assert sent(dst,pkt);
|
||||
sent(dst,pkt) := false
|
||||
}
|
||||
before recv {
|
||||
assert sent(dst,pkt);
|
||||
sent(dst,pkt) := false
|
||||
}
|
||||
}
|
||||
|
||||
instance seq_num : sequence_numbers
|
||||
|
|
@ -35,79 +35,79 @@ module transport(lower,packet,id) = {
|
|||
type mtype = {msg_t, ack_t}
|
||||
|
||||
object net_msg = {
|
||||
type t = struct {
|
||||
mty : mtype,
|
||||
src : id,
|
||||
num : seq_num.t,
|
||||
payload : packet
|
||||
}
|
||||
type t = struct {
|
||||
mty : mtype,
|
||||
src : id,
|
||||
num : seq_num.t,
|
||||
payload : packet
|
||||
}
|
||||
}
|
||||
|
||||
object impl(me:id) = {
|
||||
|
||||
|
||||
|
||||
# Create one outgoing message queue for each host
|
||||
# and a timout for each queue.
|
||||
# Create one outgoing message queue for each host
|
||||
# and a timout for each queue.
|
||||
|
||||
instance mq(D:id) : message_queue(net_msg,seq_num)
|
||||
instance timer(D:id) : timeout_sec
|
||||
instance mq(D:id) : message_queue(net_msg,seq_num)
|
||||
instance timer(D:id) : timeout_sec
|
||||
|
||||
# Keep track of the latest sequence number sent and received
|
||||
# on each channel.
|
||||
# Keep track of the latest sequence number sent and received
|
||||
# on each channel.
|
||||
|
||||
var send_seq(S:id) : seq_num.t
|
||||
var recv_seq(S:id) : seq_num.t
|
||||
var send_seq(S:id) : seq_num.t
|
||||
var recv_seq(S:id) : seq_num.t
|
||||
|
||||
init recv_seq(S) = 0 & send_seq(S) = 0
|
||||
init recv_seq(S) = 0 & send_seq(S) = 0
|
||||
|
||||
# Implementations of interface actions
|
||||
# Implementations of interface actions
|
||||
|
||||
implement send(dst:id,pkt:packet) {
|
||||
var msg : net_msg.t;
|
||||
var seq : seq_num.t;
|
||||
msg.mty := msg_t;
|
||||
msg.src := me;
|
||||
msg.num := send_seq(dst);
|
||||
msg.payload := pkt;
|
||||
send_seq(dst) := send_seq(dst).next;
|
||||
call mq(dst).enqueue(msg);
|
||||
call lower.send(me,dst,msg)
|
||||
}
|
||||
implement send(dst:id,pkt:packet) {
|
||||
var msg : net_msg.t;
|
||||
var seq : seq_num.t;
|
||||
msg.mty := msg_t;
|
||||
msg.src := me;
|
||||
msg.num := send_seq(dst);
|
||||
msg.payload := pkt;
|
||||
send_seq(dst) := send_seq(dst).next;
|
||||
call mq(dst).enqueue(msg);
|
||||
call lower.send(me,dst,msg)
|
||||
}
|
||||
|
||||
# Receiving a message is the most complicated. First, we send
|
||||
# an ack. Then, if the sequence number is correct, we call the
|
||||
# application layer action determined by the message type.
|
||||
# Receiving a message is the most complicated. First, we send
|
||||
# an ack. Then, if the sequence number is correct, we call the
|
||||
# application layer action determined by the message type.
|
||||
|
||||
implement lower.recv(msg:net_msg.t) {
|
||||
var src:id;
|
||||
var seq:seq_num.t;
|
||||
seq := msg.num;
|
||||
src := msg.src;
|
||||
if seq <= recv_seq(src) & msg.mty ~= ack_t {
|
||||
var ack : net_msg.t;
|
||||
ack.mty := ack_t;
|
||||
ack.src := me;
|
||||
ack.num := seq;
|
||||
call lower.send(me,src,ack)
|
||||
};
|
||||
if msg.mty = ack_t {
|
||||
call mq(src).delete_all(seq)
|
||||
}
|
||||
else if seq = recv_seq(src) {
|
||||
recv_seq(src) := seq_num.next(recv_seq(src));
|
||||
call recv(me,msg.payload)
|
||||
}
|
||||
}
|
||||
implement lower.recv(msg:net_msg.t) {
|
||||
var src:id;
|
||||
var seq:seq_num.t;
|
||||
seq := msg.num;
|
||||
src := msg.src;
|
||||
if seq <= recv_seq(src) & msg.mty ~= ack_t {
|
||||
var ack : net_msg.t;
|
||||
ack.mty := ack_t;
|
||||
ack.src := me;
|
||||
ack.num := seq;
|
||||
call lower.send(me,src,ack)
|
||||
};
|
||||
if msg.mty = ack_t {
|
||||
call mq(src).delete_all(seq)
|
||||
}
|
||||
else if seq = recv_seq(src) {
|
||||
recv_seq(src) := seq_num.next(recv_seq(src));
|
||||
call recv(me,msg.payload)
|
||||
}
|
||||
}
|
||||
|
||||
# If an outgoing channel times out and the queue is not empty,
|
||||
# we pick an arbitrary message in the queue and retransmit it.
|
||||
# If an outgoing channel times out and the queue is not empty,
|
||||
# we pick an arbitrary message in the queue and retransmit it.
|
||||
|
||||
implement timer.timeout(dst:id) {
|
||||
if ~mq(dst).empty {
|
||||
call lower.send(me,dst,mq(dst).pick_one)
|
||||
}
|
||||
}
|
||||
implement timer.timeout(dst:id) {
|
||||
if ~mq(dst).empty {
|
||||
call lower.send(me,dst,mq(dst).pick_one)
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
}
|
||||
|
|
|
|||
Загрузка…
Ссылка в новой задаче