crashpad works, rr gets names right, clean up antithesis folder a bit

Author: fhackett

.devcontainer/devcontainer.json

@@ -15,8 +15,7 @@
 				"golang.Go",
 				"tlaplus.vscode-ide",
 				"ms-azuretools.vscode-docker",
-				"llvm-vs-code-extensions.vscode-clangd",
-				"farrese.midas"
+				"llvm-vs-code-extensions.vscode-clangd"
 			]
 		}
 	},

antithesis/.gitignore

@@ -0,0 +1 @@
+*.log

antithesis/raftkvs/logs.zip

@@ -0,0 +1,4 @@
+FROM scratch
+
+COPY docker-compose.yaml /
+COPY model_tracelink /symbols/

antithesis/wiredtiger/Dockerfile.config

@@ -0,0 +1,13 @@
+FROM ubuntu:latest
+
+RUN apt update && apt install -y openjdk-21-jre
+
+COPY model_tracelink /workspaces/antithesis/
+COPY pgo.jar /workspaces/antithesis/
+COPY pretend_to_run.sh /workspaces/antithesis/
+COPY ./*.tla /workspaces/antithesis/
+COPY MCStorageValidate.cfg /workspaces/antithesis/
+
+COPY singleton_driver_wiredtiger.sh /opt/antithesis/test/v1/quickstart/
+
+CMD ["/workspaces/antithesis/pretend_to_run.sh"]

antithesis/wiredtiger/Dockerfile.test

@@ -0,0 +1,24 @@
+INIT Init
+NEXT Next
+
+CONSTANT
+    \* RC = "local"
+    RC ="snapshot"
+    WC = "majority"
+
+    Keys <- KeysImpl
+    MTxId <- MTxIdImpl
+    Timestamps <- TimestampsImpl
+    Node = {"n"}
+    NoValue <- NoValueImpl
+
+    __Spec!Symmetry <- SymmetryImpl
+
+    __AbortBehavior <- __AbortBehaviorImpl
+    __Action_TransactionWrite <- __Action_TransactionWriteImpl
+    __Action_TransactionRead <- __Action_TransactionReadImpl
+
+    \* Override for smaller state space.
+    IgnorePrepareOptions = {"false"}
+
+ALIAS DebugAlias

antithesis/wiredtiger/MCStorageValidate.cfg

@@ -0,0 +1,64 @@
+---- MODULE MCStorageValidate ----
+EXTENDS StorageValidate, TLC, TLCExt
+
+WT_ROLLBACK == -31800
+WT_NOTFOUND == -31803
+WT_PREPARE_CONFLICT == -31808
+
+TimestampsImpl == {} \* stub, we don't use it
+SymmetryImpl == {} \* also stub
+
+KeysImpl == TLCCache(UNION UNION { {
+    LET __rec == __traces[t][i]
+    IN  IF "k" \in DOMAIN __rec.operation
+        THEN {__rec.operation.k}
+        ELSE {}
+    : i \in DOMAIN __traces[t] }
+    : t \in DOMAIN __traces }, {"KeysImpl"})
+
+MTxIdImpl == TLCCache(UNION UNION { {
+    LET __rec == __traces[t][i]
+    IN  IF "tid" \in DOMAIN __rec.operation
+        THEN {__rec.operation.tid}
+        ELSE {}
+    : i \in DOMAIN __traces[t] }
+    : t \in DOMAIN __traces }, {"MtxIdImpl"})
+
+NoValueImpl == -1
+
+DebugAlias == __TraceOps!DebugAlias
+
+ResultCodeToTxnStatus == (
+    (WT_ROLLBACK :> __Spec!STATUS_ROLLBACK)
+    @@ (WT_NOTFOUND :> __Spec!STATUS_NOTFOUND)
+    @@ (WT_PREPARE_CONFLICT :> __Spec!STATUS_PREPARE_CONFLICT) 
+)
+
+__AbortBehaviorImpl ==
+    CASE __action'.operation_name = "TransactionWrite" ->
+            /\ __action'.operation._meta.result_code # 0
+            /\ __Spec!TransactionWrite(__action'.operation.n, __action'.operation.tid, __action'.operation.k, __action'.operation.v, __action'.operation.ignoreWriteConflicts)
+            /\ txnStatus'["n"][__action'.operation.tid] = ResultCodeToTxnStatus[__action'.operation._meta.result_code]
+      [] __action'.operation_name = "TransactionRead" ->
+            /\ __action'.operation._meta.result_code # 0
+            /\ __Spec!TransactionRead(__action'.operation.n, __action'.operation.tid, __action'.operation.k, __action'.operation.v)
+            /\ txnStatus'["n"][__action'.operation.tid] = ResultCodeToTxnStatus[__action'.operation._meta.result_code]
+      [] __action'.operation_name = "TransactionRemove" ->
+            /\ __action'.operation._meta.result_code # 0
+            /\ __Spec!TransactionRemove(__action'.operation.n, __action'.operation.tid, __action'.operation.k)
+            /\ txnStatus'["n"][__action'.operation.tid] = ResultCodeToTxnStatus[__action'.operation._meta.result_code]
+      [] OTHER -> UNCHANGED __Spec_vars
+
+__Action_TransactionWriteImpl ==
+    /\ __action'.operation._meta.result_code = 0
+    /\ txnStatus'["n"][__action'.operation.tid] = "OK"
+
+__Action_TransactionReadImpl ==
+    /\ __action'.operation._meta.result_code = 0
+    /\ txnStatus'["n"][__action'.operation.tid] = "OK"
+
+__Action_TransactionRemoveImpl ==
+    /\ __action'.operation._meta.result_code = 0
+    /\ txnStatus'["n"][__action'.operation.tid] = "OK"
+
+====