Update gold

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");;
  #().

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 :=

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";

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.