From 6787e01cef93d900c0018ed84f44141f26d1fbb9 Mon Sep 17 00:00:00 2001 From: Tej Chajed Date: Sat, 7 Sep 2024 11:06:35 -0500 Subject: [PATCH] Update gold --- .../examples/append_log/append_log.gold.v | 18 +++---- internal/examples/logging2/logging2.gold.v | 26 +++++----- internal/examples/semantics/semantics.gold.v | 20 ++++---- internal/examples/simpledb/simpledb.gold.v | 48 +++++++++---------- internal/examples/unittest/unittest.gold.v | 42 ++++++++-------- internal/examples/wal/wal.gold.v | 8 ++-- 6 files changed, 81 insertions(+), 81 deletions(-) diff --git a/internal/examples/append_log/append_log.gold.v b/internal/examples/append_log/append_log.gold.v index 20b1fc8..6d6cd5d 100644 --- a/internal/examples/append_log/append_log.gold.v +++ b/internal/examples/append_log/append_log.gold.v @@ -33,13 +33,13 @@ Definition Init: val := (if: "diskSz" < #1 then (struct.new Log [ - "m" ::= lock.new #(); + "m" ::= newMutex #(); "sz" ::= #0; "diskSz" ::= #0 ], #false) else let: "log" := struct.new Log [ - "m" ::= lock.new #(); + "m" ::= newMutex #(); "sz" ::= #0; "diskSz" ::= "diskSz" ] in @@ -53,7 +53,7 @@ Definition Open: val := let: "sz" := marshal.Dec__GetInt "dec" in let: "diskSz" := marshal.Dec__GetInt "dec" in struct.new Log [ - "m" ::= lock.new #(); + "m" ::= newMutex #(); "sz" ::= "sz"; "diskSz" ::= "diskSz" ]. @@ -67,9 +67,9 @@ Definition Log__get: val := Definition Log__Get: val := rec: "Log__Get" "log" "i" := - lock.acquire (struct.loadF Log "m" "log");; + Mutex__Lock (struct.loadF Log "m" "log");; let: ("v", "b") := Log__get "log" "i" in - lock.release (struct.loadF Log "m" "log");; + Mutex__Unlock (struct.loadF Log "m" "log");; ("v", "b"). Definition writeAll: val := @@ -91,9 +91,9 @@ Definition Log__append: val := Definition Log__Append: val := rec: "Log__Append" "log" "bks" := - lock.acquire (struct.loadF Log "m" "log");; + Mutex__Lock (struct.loadF Log "m" "log");; let: "b" := Log__append "log" "bks" in - lock.release (struct.loadF Log "m" "log");; + Mutex__Unlock (struct.loadF Log "m" "log");; "b". Definition Log__reset: val := @@ -104,7 +104,7 @@ Definition Log__reset: val := Definition Log__Reset: val := rec: "Log__Reset" "log" := - lock.acquire (struct.loadF Log "m" "log");; + Mutex__Lock (struct.loadF Log "m" "log");; Log__reset "log";; - lock.release (struct.loadF Log "m" "log");; + Mutex__Unlock (struct.loadF Log "m" "log");; #(). diff --git a/internal/examples/logging2/logging2.gold.v b/internal/examples/logging2/logging2.gold.v index 1dc8945..bcc556f 100644 --- a/internal/examples/logging2/logging2.gold.v +++ b/internal/examples/logging2/logging2.gold.v @@ -33,8 +33,8 @@ Definition Log__writeHdr: val := Definition Init: val := rec: "Init" "logSz" := let: "log" := struct.mk Log [ - "logLock" ::= lock.new #(); - "memLock" ::= lock.new #(); + "logLock" ::= newMutex #(); + "memLock" ::= newMutex #(); "logSz" ::= "logSz"; "memLog" ::= ref (zero_val (slice.T disk.blockT)); "memLen" ::= ref (zero_val uint64T); @@ -62,10 +62,10 @@ Definition Log__readBlocks: val := Definition Log__Read: val := rec: "Log__Read" "log" := - lock.acquire (struct.get Log "logLock" "log");; + Mutex__Lock (struct.get Log "logLock" "log");; let: "disklen" := Log__readHdr "log" in let: "blks" := Log__readBlocks "log" "disklen" in - lock.release (struct.get Log "logLock" "log");; + Mutex__Unlock (struct.get Log "logLock" "log");; "blks". Definition Log__memWrite: val := @@ -79,25 +79,25 @@ Definition Log__memWrite: val := Definition Log__memAppend: val := rec: "Log__memAppend" "log" "l" := - lock.acquire (struct.get Log "memLock" "log");; + Mutex__Lock (struct.get Log "memLock" "log");; (if: ((![uint64T] (struct.get Log "memLen" "log")) + (slice.len "l")) ≥ (struct.get Log "logSz" "log") then - lock.release (struct.get Log "memLock" "log");; + Mutex__Unlock (struct.get Log "memLock" "log");; (#false, #0) else let: "txn" := ![uint64T] (struct.get Log "memTxnNxt" "log") in let: "n" := (![uint64T] (struct.get Log "memLen" "log")) + (slice.len "l") in (struct.get Log "memLen" "log") <-[uint64T] "n";; (struct.get Log "memTxnNxt" "log") <-[uint64T] ((![uint64T] (struct.get Log "memTxnNxt" "log")) + #1);; - lock.release (struct.get Log "memLock" "log");; + Mutex__Unlock (struct.get Log "memLock" "log");; (#true, "txn")). (* XXX just an atomic read? *) Definition Log__readLogTxnNxt: val := rec: "Log__readLogTxnNxt" "log" := - lock.acquire (struct.get Log "memLock" "log");; + Mutex__Lock (struct.get Log "memLock" "log");; let: "n" := ![uint64T] (struct.get Log "logTxnNxt" "log") in - lock.release (struct.get Log "memLock" "log");; + Mutex__Unlock (struct.get Log "memLock" "log");; "n". Definition Log__diskAppendWait: val := @@ -130,18 +130,18 @@ Definition Log__writeBlocks: val := Definition Log__diskAppend: val := rec: "Log__diskAppend" "log" := - lock.acquire (struct.get Log "logLock" "log");; + Mutex__Lock (struct.get Log "logLock" "log");; let: "disklen" := Log__readHdr "log" in - lock.acquire (struct.get Log "memLock" "log");; + Mutex__Lock (struct.get Log "memLock" "log");; let: "memlen" := ![uint64T] (struct.get Log "memLen" "log") in let: "allblks" := ![slice.T (slice.T byteT)] (struct.get Log "memLog" "log") in let: "blks" := SliceSkip (slice.T byteT) "allblks" "disklen" in let: "memnxt" := ![uint64T] (struct.get Log "memTxnNxt" "log") in - lock.release (struct.get Log "memLock" "log");; + Mutex__Unlock (struct.get Log "memLock" "log");; Log__writeBlocks "log" "blks" "disklen";; Log__writeHdr "log" "memlen";; (struct.get Log "logTxnNxt" "log") <-[uint64T] "memnxt";; - lock.release (struct.get Log "logLock" "log");; + Mutex__Unlock (struct.get Log "logLock" "log");; #(). Definition Log__Logger: val := diff --git a/internal/examples/semantics/semantics.gold.v b/internal/examples/semantics/semantics.gold.v index 00fad26..6fdeb95 100644 --- a/internal/examples/semantics/semantics.gold.v +++ b/internal/examples/semantics/semantics.gold.v @@ -566,9 +566,9 @@ Definition testIfStmtInterface: val := locks are correctly interpreted *) Definition testsUseLocks: val := rec: "testsUseLocks" <> := - let: "m" := lock.new #() in - lock.acquire "m";; - lock.release "m";; + let: "m" := newMutex #() in + Mutex__Lock "m";; + Mutex__Unlock "m";; #true. (* loops.go *) @@ -1036,10 +1036,10 @@ Definition testShiftMod: val := Definition testLinearize: val := rec: "testLinearize" <> := - let: "m" := lock.new #() in - lock.acquire "m";; + let: "m" := newMutex #() in + Mutex__Lock "m";; Linearize;; - lock.release "m";; + Mutex__Unlock "m";; #true. (* shortcircuiting.go *) @@ -1474,7 +1474,7 @@ Definition New: val := disk.Write #0 "header";; let: "lengthPtr" := ref (zero_val uint64T) in "lengthPtr" <-[uint64T] #0;; - let: "l" := lock.new #() in + let: "l" := newMutex #() in struct.mk Log [ "d" ::= "d"; "cache" ::= "cache"; @@ -1484,12 +1484,12 @@ Definition New: val := Definition Log__lock: val := rec: "Log__lock" "l" := - lock.acquire (struct.get Log "l" "l");; + Mutex__Lock (struct.get Log "l" "l");; #(). Definition Log__unlock: val := rec: "Log__unlock" "l" := - lock.release (struct.get Log "l" "l");; + Mutex__Unlock (struct.get Log "l" "l");; #(). (* BeginTxn allocates space for a new transaction in the log. @@ -1607,7 +1607,7 @@ Definition Open: val := let: "cache" := NewMap uint64T disk.blockT #() in let: "lengthPtr" := ref (zero_val uint64T) in "lengthPtr" <-[uint64T] #0;; - let: "l" := lock.new #() in + let: "l" := newMutex #() in struct.mk Log [ "d" ::= "d"; "cache" ::= "cache"; diff --git a/internal/examples/simpledb/simpledb.gold.v b/internal/examples/simpledb/simpledb.gold.v index aee60a6..39f55a5 100644 --- a/internal/examples/simpledb/simpledb.gold.v +++ b/internal/examples/simpledb/simpledb.gold.v @@ -282,15 +282,15 @@ Definition NewDb: val := rec: "NewDb" <> := let: "wbuf" := makeValueBuffer #() in let: "rbuf" := makeValueBuffer #() in - let: "bufferL" := lock.new #() in + let: "bufferL" := newMutex #() in let: "tableName" := #(str"table.0") in let: "tableNameRef" := ref (zero_val stringT) in "tableNameRef" <-[stringT] "tableName";; let: "table" := CreateTable "tableName" in let: "tableRef" := struct.alloc Table (zero_val (struct.t Table)) in struct.store Table "tableRef" "table";; - let: "tableL" := lock.new #() in - let: "compactionL" := lock.new #() in + let: "tableL" := newMutex #() in + let: "compactionL" := newMutex #() in struct.mk Database [ "wbuffer" ::= "wbuf"; "rbuffer" ::= "rbuf"; @@ -309,26 +309,26 @@ Definition NewDb: val := Reflects any completed in-memory writes. *) Definition Read: val := rec: "Read" "db" "k" := - lock.acquire (struct.get Database "bufferL" "db");; + Mutex__Lock (struct.get Database "bufferL" "db");; let: "buf" := ![mapT (slice.T byteT)] (struct.get Database "wbuffer" "db") in let: ("v", "ok") := MapGet "buf" "k" in (if: "ok" then - lock.release (struct.get Database "bufferL" "db");; + Mutex__Unlock (struct.get Database "bufferL" "db");; ("v", #true) else let: "rbuf" := ![mapT (slice.T byteT)] (struct.get Database "rbuffer" "db") in let: ("v2", "ok") := MapGet "rbuf" "k" in (if: "ok" then - lock.release (struct.get Database "bufferL" "db");; + Mutex__Unlock (struct.get Database "bufferL" "db");; ("v2", #true) else - lock.acquire (struct.get Database "tableL" "db");; + Mutex__Lock (struct.get Database "tableL" "db");; let: "tbl" := struct.load Table (struct.get Database "table" "db") in let: ("v3", "ok") := tableRead "tbl" "k" in - lock.release (struct.get Database "tableL" "db");; - lock.release (struct.get Database "bufferL" "db");; + Mutex__Unlock (struct.get Database "tableL" "db");; + Mutex__Unlock (struct.get Database "bufferL" "db");; ("v3", "ok"))). (* Write sets a key to a new value. @@ -339,10 +339,10 @@ Definition Read: val := The new value is buffered in memory. To persist it, call db.Compact(). *) Definition Write: val := rec: "Write" "db" "k" "v" := - lock.acquire (struct.get Database "bufferL" "db");; + Mutex__Lock (struct.get Database "bufferL" "db");; let: "buf" := ![mapT (slice.T byteT)] (struct.get Database "wbuffer" "db") in MapInsert "buf" "k" "v";; - lock.release (struct.get Database "bufferL" "db");; + Mutex__Unlock (struct.get Database "bufferL" "db");; #(). Definition freshTable: val := @@ -417,14 +417,14 @@ Definition constructNewTable: val := writes with existing writes. *) Definition Compact: val := rec: "Compact" "db" := - lock.acquire (struct.get Database "compactionL" "db");; - lock.acquire (struct.get Database "bufferL" "db");; + Mutex__Lock (struct.get Database "compactionL" "db");; + Mutex__Lock (struct.get Database "bufferL" "db");; let: "buf" := ![mapT (slice.T byteT)] (struct.get Database "wbuffer" "db") in let: "emptyWbuffer" := NewMap uint64T (slice.T byteT) #() in (struct.get Database "wbuffer" "db") <-[mapT (slice.T byteT)] "emptyWbuffer";; (struct.get Database "rbuffer" "db") <-[mapT (slice.T byteT)] "buf";; - lock.release (struct.get Database "bufferL" "db");; - lock.acquire (struct.get Database "tableL" "db");; + Mutex__Unlock (struct.get Database "bufferL" "db");; + Mutex__Lock (struct.get Database "tableL" "db");; let: "oldTableName" := ![stringT] (struct.get Database "tableName" "db") in let: ("oldTable", "t") := constructNewTable "db" "buf" in let: "newTable" := freshTable "oldTableName" in @@ -434,8 +434,8 @@ Definition Compact: val := FS.atomicCreate #(str"db") #(str"manifest") "manifestData";; CloseTable "oldTable";; FS.delete #(str"db") "oldTableName";; - lock.release (struct.get Database "tableL" "db");; - lock.release (struct.get Database "compactionL" "db");; + Mutex__Unlock (struct.get Database "tableL" "db");; + Mutex__Unlock (struct.get Database "compactionL" "db");; #(). Definition recoverManifest: val := @@ -485,9 +485,9 @@ Definition Recover: val := deleteOtherFiles "tableName";; let: "wbuffer" := makeValueBuffer #() in let: "rbuffer" := makeValueBuffer #() in - let: "bufferL" := lock.new #() in - let: "tableL" := lock.new #() in - let: "compactionL" := lock.new #() in + let: "bufferL" := newMutex #() in + let: "tableL" := newMutex #() in + let: "compactionL" := newMutex #() in struct.mk Database [ "wbuffer" ::= "wbuffer"; "rbuffer" ::= "rbuffer"; @@ -504,12 +504,12 @@ Definition Recover: val := cleanly closing any open files. *) Definition Shutdown: val := rec: "Shutdown" "db" := - lock.acquire (struct.get Database "bufferL" "db");; - lock.acquire (struct.get Database "compactionL" "db");; + Mutex__Lock (struct.get Database "bufferL" "db");; + Mutex__Lock (struct.get Database "compactionL" "db");; let: "t" := struct.load Table (struct.get Database "table" "db") in CloseTable "t";; - lock.release (struct.get Database "compactionL" "db");; - lock.release (struct.get Database "bufferL" "db");; + Mutex__Unlock (struct.get Database "compactionL" "db");; + Mutex__Unlock (struct.get Database "bufferL" "db");; #(). (* Close closes an open database cleanly, flushing any in-memory writes. diff --git a/internal/examples/unittest/unittest.gold.v b/internal/examples/unittest/unittest.gold.v index b39c6f2..d3b3b01 100644 --- a/internal/examples/unittest/unittest.gold.v +++ b/internal/examples/unittest/unittest.gold.v @@ -37,10 +37,10 @@ Definition hasEndComment: val := Definition condvarWrapping: val := rec: "condvarWrapping" <> := let: "mu" := ref (zero_val ptrT) in - "mu" <-[ptrT] (lock.new #());; - let: "cond1" := lock.newCond (![ptrT] "mu") in - "mu" <-[ptrT] (lock.new #());; - lock.condWait "cond1";; + "mu" <-[ptrT] (newMutex #());; + let: "cond1" := NewCond (![ptrT] "mu") in + "mu" <-[ptrT] (newMutex #());; + Cond__Wait "cond1";; #(). (* const.go *) @@ -419,19 +419,19 @@ Definition compositeLitLenZero: val := Definition useLocks: val := rec: "useLocks" <> := - let: "m" := lock.new #() in - lock.acquire "m";; - lock.release "m";; + let: "m" := newMutex #() in + Mutex__Lock "m";; + Mutex__Unlock "m";; #(). Definition useCondVar: val := rec: "useCondVar" <> := - let: "m" := lock.new #() in - let: "c" := lock.newCond "m" in - lock.acquire "m";; - lock.condSignal "c";; - lock.condWait "c";; - lock.release "m";; + let: "m" := newMutex #() in + let: "c" := NewCond "m" in + Mutex__Lock "m";; + Cond__Signal "c";; + Cond__Wait "c";; + Mutex__Unlock "m";; #(). Definition hasCondVar := struct.decl [ @@ -906,17 +906,17 @@ Definition Skip: val := Definition simpleSpawn: val := rec: "simpleSpawn" <> := - let: "l" := lock.new #() in + let: "l" := newMutex #() in let: "v" := ref (zero_val uint64T) in - Fork (lock.acquire "l";; + Fork (Mutex__Lock "l";; let: "x" := ![uint64T] "v" in (if: "x" > #0 then Skip #() else #());; - lock.release "l");; - lock.acquire "l";; + Mutex__Unlock "l");; + Mutex__Lock "l";; "v" <-[uint64T] #1;; - lock.release "l";; + Mutex__Unlock "l";; #(). Definition threadCode: val := @@ -1047,13 +1047,13 @@ Definition setField: val := (* DoSomeLocking uses the entire lock API *) Definition DoSomeLocking: val := rec: "DoSomeLocking" "l" := - lock.acquire "l";; - lock.release "l";; + Mutex__Lock "l";; + Mutex__Unlock "l";; #(). Definition makeLock: val := rec: "makeLock" <> := - let: "l" := lock.new #() in + let: "l" := newMutex #() in DoSomeLocking "l";; #(). diff --git a/internal/examples/wal/wal.gold.v b/internal/examples/wal/wal.gold.v index dae8508..95c13cc 100644 --- a/internal/examples/wal/wal.gold.v +++ b/internal/examples/wal/wal.gold.v @@ -39,7 +39,7 @@ Definition New: val := disk.Write #0 "header";; let: "lengthPtr" := ref (zero_val uint64T) in "lengthPtr" <-[uint64T] #0;; - let: "l" := lock.new #() in + let: "l" := newMutex #() in struct.mk Log [ "d" ::= "d"; "cache" ::= "cache"; @@ -49,12 +49,12 @@ Definition New: val := Definition Log__lock: val := rec: "Log__lock" "l" := - lock.acquire (struct.get Log "l" "l");; + Mutex__Lock (struct.get Log "l" "l");; #(). Definition Log__unlock: val := rec: "Log__unlock" "l" := - lock.release (struct.get Log "l" "l");; + Mutex__Unlock (struct.get Log "l" "l");; #(). (* BeginTxn allocates space for a new transaction in the log. @@ -172,7 +172,7 @@ Definition Open: val := let: "cache" := NewMap uint64T disk.blockT #() in let: "lengthPtr" := ref (zero_val uint64T) in "lengthPtr" <-[uint64T] #0;; - let: "l" := lock.new #() in + let: "l" := newMutex #() in struct.mk Log [ "d" ::= "d"; "cache" ::= "cache";