Skip to content

Commit

Permalink
Prove tulip network except for commit and abort
Browse files Browse the repository at this point in the history
  • Loading branch information
@yunshengtw
yunshengtw committed Nov 24, 2024
1 parent 7981b0e commit 04e1dd2
Show file tree
Hide file tree
Showing 26 changed files with 2,392 additions and 152 deletions.
58 changes: 40 additions & 18 deletions external/Goose/github_com/mit_pdos/tulip/gcoord.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -95,18 +95,21 @@ Definition GroupCoordinator__Send: val :=
rec: "GroupCoordinator__Send" "gcoord" "rid" "data" :=
let: ("conn", "ok") := GroupCoordinator__GetConnection "gcoord" "rid" in
(if: (~ "ok")
then GroupCoordinator__Connect "gcoord" "rid"
else #());;
let: "err" := grove_ffi.Send "conn" "data" in
(if: "err"
then
GroupCoordinator__Connect "gcoord" "rid";;
#()
else #()).
else
let: "err" := grove_ffi.Send "conn" "data" in
(if: "err"
then
GroupCoordinator__Connect "gcoord" "rid";;
#()
else #())).

Definition GroupCoordinator__SendRead: val :=
rec: "GroupCoordinator__SendRead" "gcoord" "rid" "ts" "key" :=
GroupCoordinator__Send "gcoord" "rid" (message.EncodeTxnRead "ts" "key");;
let: "data" := message.EncodeTxnReadRequest "ts" "key" in
GroupCoordinator__Send "gcoord" "rid" "data";;
#().

Definition GroupCoordinator__ReadSession: val :=
Expand Down Expand Up @@ -254,27 +257,38 @@ Definition GroupCoordinator__NextPrepareAction: val :=

Definition GroupCoordinator__SendFastPrepare: val :=
rec: "GroupCoordinator__SendFastPrepare" "gcoord" "rid" "ts" "pwrs" "ptgs" :=
GroupCoordinator__Send "gcoord" "rid" (message.EncodeTxnFastPrepare "ts" "pwrs" "ptgs");;
let: "data" := message.EncodeTxnFastPrepareRequest "ts" "pwrs" "ptgs" in
GroupCoordinator__Send "gcoord" "rid" "data";;
#().

Definition GroupCoordinator__SendValidate: val :=
rec: "GroupCoordinator__SendValidate" "gcoord" "rid" "ts" "rank" "pwrs" "ptgs" :=
let: "data" := message.EncodeTxnValidateRequest "ts" "rank" "pwrs" "ptgs" in
GroupCoordinator__Send "gcoord" "rid" "data";;
#().

Definition GroupCoordinator__SendPrepare: val :=
rec: "GroupCoordinator__SendPrepare" "gcoord" "rid" "ts" "rank" :=
let: "data" := message.EncodeTxnPrepareRequest "ts" "rank" in
GroupCoordinator__Send "gcoord" "rid" "data";;
#().

Definition GroupCoordinator__SendUnprepare: val :=
rec: "GroupCoordinator__SendUnprepare" "gcoord" "rid" "ts" "rank" :=
let: "data" := message.EncodeTxnUnprepareRequest "ts" "rank" in
GroupCoordinator__Send "gcoord" "rid" "data";;
#().

Definition GroupCoordinator__SendQuery: val :=
rec: "GroupCoordinator__SendQuery" "gcoord" "rid" "ts" "rank" :=
let: "data" := message.EncodeTxnQueryRequest "ts" "rank" in
GroupCoordinator__Send "gcoord" "rid" "data";;
#().

Definition GroupCoordinator__SendRefresh: val :=
rec: "GroupCoordinator__SendRefresh" "gcoord" "rid" "ts" "rank" :=
let: "data" := message.EncodeTxnRefreshRequest "ts" "rank" in
GroupCoordinator__Send "gcoord" "rid" "data";;
#().

Definition GroupCoordinator__PrepareSession: val :=
Expand Down Expand Up @@ -393,6 +407,8 @@ Definition GroupCoordinator__Finalized: val :=

Definition GroupCoordinator__SendCommit: val :=
rec: "GroupCoordinator__SendCommit" "gcoord" "rid" "ts" "pwrs" :=
let: "data" := message.EncodeTxnCommitRequest "ts" "pwrs" in
GroupCoordinator__Send "gcoord" "rid" "data";;
#().

Definition GroupCoordinator__ChangeLeader: val :=
Expand All @@ -417,6 +433,8 @@ Definition GroupCoordinator__Commit: val :=

Definition GroupCoordinator__SendAbort: val :=
rec: "GroupCoordinator__SendAbort" "gcoord" "rid" "ts" :=
let: "data" := message.EncodeTxnAbortRequest "ts" in
GroupCoordinator__Send "gcoord" "rid" "data";;
#().

Definition GroupCoordinator__Abort: val :=
Expand Down Expand Up @@ -679,12 +697,12 @@ Definition GroupPreparer__processUnprepareResult: val :=
else #()))).

Definition GroupPreparer__processQueryResult: val :=
rec: "GroupPreparer__processQueryResult" "gpp" "rid" "res" :=
rec: "GroupPreparer__processQueryResult" "gpp" "res" :=
GroupPreparer__tryResign "gpp" "res";;
#().

Definition GroupCoordinator__ResultSession: val :=
rec: "GroupCoordinator__ResultSession" "gcoord" "rid" :=
Definition GroupCoordinator__ResponseSession: val :=
rec: "GroupCoordinator__ResponseSession" "gcoord" "rid" :=
Skip;;
(for: (λ: <>, #true); (λ: <>, Skip) := λ: <>,
let: ("data", "ok") := GroupCoordinator__Receive "gcoord" "rid" in
Expand All @@ -707,25 +725,29 @@ Definition GroupCoordinator__ResultSession: val :=
Mutex__Unlock (struct.loadF GroupCoordinator "mu" "gcoord");;
Continue
else
let: "gpp" := struct.loadF GroupCoordinator "gpp" "gcoord" in
let: "grd" := struct.loadF GroupCoordinator "grd" "gcoord" in
(if: "kind" = message.MSG_TXN_READ
then GroupReader__processReadResult "grd" "rid" (struct.get message.TxnResponse "Key" "msg") (struct.get message.TxnResponse "Version" "msg")
then GroupReader__processReadResult (struct.loadF GroupCoordinator "grd" "gcoord") (struct.get message.TxnResponse "ReplicaID" "msg") (struct.get message.TxnResponse "Key" "msg") (struct.get message.TxnResponse "Version" "msg")
else
(if: "kind" = message.MSG_TXN_FAST_PREPARE
then GroupPreparer__processFastPrepareResult "gpp" "rid" (struct.get message.TxnResponse "Result" "msg")
then GroupPreparer__processFastPrepareResult (struct.loadF GroupCoordinator "gpp" "gcoord") (struct.get message.TxnResponse "ReplicaID" "msg") (struct.get message.TxnResponse "Result" "msg")
else
(if: "kind" = message.MSG_TXN_VALIDATE
then GroupPreparer__processValidateResult "gpp" "rid" (struct.get message.TxnResponse "Result" "msg")
then GroupPreparer__processValidateResult (struct.loadF GroupCoordinator "gpp" "gcoord") (struct.get message.TxnResponse "ReplicaID" "msg") (struct.get message.TxnResponse "Result" "msg")
else
(if: "kind" = message.MSG_TXN_PREPARE
then GroupPreparer__processPrepareResult "gpp" "rid" (struct.get message.TxnResponse "Result" "msg")
then
(if: (struct.get message.TxnResponse "Rank" "msg") = #1
then GroupPreparer__processPrepareResult (struct.loadF GroupCoordinator "gpp" "gcoord") (struct.get message.TxnResponse "ReplicaID" "msg") (struct.get message.TxnResponse "Result" "msg")
else #())
else
(if: "kind" = message.MSG_TXN_UNPREPARE
then GroupPreparer__processUnprepareResult "gpp" "rid" (struct.get message.TxnResponse "Result" "msg")
then
(if: (struct.get message.TxnResponse "Rank" "msg") = #1
then GroupPreparer__processUnprepareResult (struct.loadF GroupCoordinator "gpp" "gcoord") (struct.get message.TxnResponse "ReplicaID" "msg") (struct.get message.TxnResponse "Result" "msg")
else #())
else
(if: "kind" = message.MSG_TXN_QUERY
then GroupPreparer__processQueryResult "gpp" "rid" (struct.get message.TxnResponse "Result" "msg")
then GroupPreparer__processQueryResult (struct.loadF GroupCoordinator "gpp" "gcoord") (struct.get message.TxnResponse "Result" "msg")
else
(if: "kind" = message.MSG_TXN_REFRESH
then #()
Expand Down
157 changes: 152 additions & 5 deletions external/Goose/github_com/mit_pdos/tulip/message.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,14 +8,16 @@ Context `{ext_ty: ext_types}.
Definition TxnRequest := struct.decl [
"Kind" :: uint64T;
"Timestamp" :: uint64T;
"Key" :: stringT;
"Rank" :: uint64T;
"PartialWrites" :: tulip.KVMap;
"PartialWrites" :: slice.T (struct.t tulip.WriteEntry);
"ParticipantGroups" :: slice.T uint64T
].

Definition TxnResponse := struct.decl [
"Kind" :: uint64T;
"Timestamp" :: uint64T;
"ReplicaID" :: uint64T;
"Result" :: uint64T;
"Key" :: stringT;
"Version" :: struct.t tulip.Version;
Expand Down Expand Up @@ -45,14 +47,159 @@ Definition MSG_TXN_COMMIT : expr := #300.

Definition MSG_TXN_ABORT : expr := #301.

Definition EncodeTxnRead: val :=
rec: "EncodeTxnRead" "ts" "key" :=
Definition EncodeTxnReadRequest: val :=
rec: "EncodeTxnReadRequest" "ts" "key" :=
slice.nil.

Definition DecodeTxnReadRequest: val :=
rec: "DecodeTxnReadRequest" "data" :=
struct.mk TxnRequest [
].

Definition EncodeTxnReadResponse: val :=
rec: "EncodeTxnReadResponse" "ts" "rid" "key" "lts" "value" :=
slice.nil.

Definition DecodeTxnReadResponse: val :=
rec: "DecodeTxnReadResponse" "data" :=
struct.mk TxnResponse [
].

Definition EncodeTxnFastPrepareRequest: val :=
rec: "EncodeTxnFastPrepareRequest" "ts" "pwrs" "ptgs" :=
slice.nil.

Definition DecodeTxnFastPrepareRequest: val :=
rec: "DecodeTxnFastPrepareRequest" "data" :=
struct.mk TxnRequest [
].

Definition EncodeTxnFastPrepareResponse: val :=
rec: "EncodeTxnFastPrepareResponse" "ts" "rid" "res" :=
slice.nil.

Definition DecodeTxnFastPrepareResponse: val :=
rec: "DecodeTxnFastPrepareResponse" "data" :=
struct.mk TxnResponse [
].

Definition EncodeTxnValidateRequest: val :=
rec: "EncodeTxnValidateRequest" "ts" "rank" "pwrs" "ptgs" :=
slice.nil.

Definition DecodeTxnValidateRequest: val :=
rec: "DecodeTxnValidateRequest" "data" :=
struct.mk TxnRequest [
].

Definition EncodeTxnValidateResponse: val :=
rec: "EncodeTxnValidateResponse" "ts" "rid" "res" :=
slice.nil.

Definition DecodeTxnValidateResponse: val :=
rec: "DecodeTxnValidateResponse" "data" :=
struct.mk TxnResponse [
].

Definition EncodeTxnPrepareRequest: val :=
rec: "EncodeTxnPrepareRequest" "ts" "rank" :=
slice.nil.

Definition DecodeTxnPrepareRequest: val :=
rec: "DecodeTxnPrepareRequest" "data" :=
struct.mk TxnRequest [
].

Definition EncodeTxnPrepareResponse: val :=
rec: "EncodeTxnPrepareResponse" "ts" "rank" "rid" "res" :=
slice.nil.

Definition DecodeTxnPrepareResponse: val :=
rec: "DecodeTxnPrepareResponse" "data" :=
struct.mk TxnResponse [
].

Definition EncodeTxnUnprepareRequest: val :=
rec: "EncodeTxnUnprepareRequest" "ts" "rank" :=
slice.nil.

Definition EncodeTxnFastPrepare: val :=
rec: "EncodeTxnFastPrepare" "ts" "pwrs" "ptgs" :=
Definition DecodeTxnUnprepareRequest: val :=
rec: "DecodeTxnUnprepareRequest" "data" :=
struct.mk TxnRequest [
].

Definition EncodeTxnUnprepareResponse: val :=
rec: "EncodeTxnUnprepareResponse" "ts" "rank" "rid" "res" :=
slice.nil.

Definition DecodeTxnUnprepareResponse: val :=
rec: "DecodeTxnUnprepareResponse" "data" :=
struct.mk TxnResponse [
].

Definition EncodeTxnQueryRequest: val :=
rec: "EncodeTxnQueryRequest" "ts" "rank" :=
slice.nil.

Definition DecodeTxnQueryRequest: val :=
rec: "DecodeTxnQueryRequest" "data" :=
struct.mk TxnRequest [
].

Definition EncodeTxnQueryResponse: val :=
rec: "EncodeTxnQueryResponse" "ts" "res" :=
slice.nil.

Definition DecodeTxnQueryResponse: val :=
rec: "DecodeTxnQueryResponse" "data" :=
struct.mk TxnResponse [
].

Definition EncodeTxnRefreshRequest: val :=
rec: "EncodeTxnRefreshRequest" "ts" "rank" :=
slice.nil.

Definition DecodeTxnRefreshRequest: val :=
rec: "DecodeTxnRefreshRequest" "data" :=
struct.mk TxnRequest [
].

Definition EncodeTxnCommitRequest: val :=
rec: "EncodeTxnCommitRequest" "ts" "pwrs" :=
slice.nil.

Definition DecodeTxnCommitRequest: val :=
rec: "DecodeTxnCommitRequest" "data" :=
struct.mk TxnRequest [
].

Definition EncodeTxnCommitResponse: val :=
rec: "EncodeTxnCommitResponse" "ts" "res" :=
slice.nil.

Definition DecodeTxnCommitResponse: val :=
rec: "DecodeTxnCommitResponse" "data" :=
struct.mk TxnResponse [
].

Definition EncodeTxnAbortRequest: val :=
rec: "EncodeTxnAbortRequest" "ts" :=
slice.nil.

Definition DecodeTxnAbortRequest: val :=
rec: "DecodeTxnAbortRequest" "data" :=
struct.mk TxnRequest [
].

Definition EncodeTxnAbortResponse: val :=
rec: "EncodeTxnAbortResponse" "ts" "res" :=
slice.nil.

Definition DecodeTxnAbortResponse: val :=
rec: "DecodeTxnAbortResponse" "data" :=
struct.mk TxnResponse [
].

Definition DecodeTxnRequest: val :=
rec: "DecodeTxnRequest" "data" :=
struct.mk TxnRequest [
Expand Down
Loading

0 comments on commit 04e1dd2

Please sign in to comment.