fix compilation issues

Author: tjhance

concurrency/framework/DiskExtern.h

@@ -75,6 +75,15 @@ namespace InstantiatedDiskInterface {
     }
   }
 
+  inline void sync__write(Ptrs::Ptr buf, uint64 nbytes, int64_t offset)
+  {
+    int ret = pwrite(fd, (void*)buf.ptr, nbytes, offset * 4096);
+    if (ret != nbytes) {
+      std::cerr << "pwrite failed " << ret << std::endl;
+      exit(1);
+    }
+  }
+
   inline Ptrs::Ptr get__event(IOCtx& ioctx) {
     struct io_event event;
     int status = io_getevents(*ioctx.ctx, 0, 1, &event, NULL);

concurrency/scache/cache/CacheSM.i.dfy

@@ -409,15 +409,15 @@ module CacheSSM refines DiskSSM(CacheIfc) {
   }
 
   datatype Step =
-    | StartReadStep(cache_idx: nat, disk_idx: nat)
-    | FinishReadStep(cache_idx: nat, disk_idx: nat)
-    | StartWritebackStep(cache_idx: nat)
-    | FinishWritebackStep(cache_idx: nat)
-    | EvictStep(cache_idx: nat)
-    | ObserveCleanForSyncStep(cache_idx: nat, rid: RequestId)
-    | ApplyReadStep(cache_idx: nat, rid: RequestId)
-    | ApplyWriteStep(cache_idx: nat, rid: RequestId)
-    | MarkDirtyStep(cache_idx: nat)
+    | StartReadStep(ghost cache_idx: nat, ghost disk_idx: nat)
+    | FinishReadStep(ghost cache_idx: nat, ghost disk_idx: nat)
+    | StartWritebackStep(ghost cache_idx: nat)
+    | FinishWritebackStep(ghost cache_idx: nat)
+    | EvictStep(ghost cache_idx: nat)
+    | ObserveCleanForSyncStep(ghost cache_idx: nat, ghost rid: RequestId)
+    | ApplyReadStep(ghost cache_idx: nat, ghost rid: RequestId)
+    | ApplyWriteStep(ghost cache_idx: nat, ghost rid: RequestId)
+    | MarkDirtyStep(ghost cache_idx: nat)
 
   predicate InternalStep(shard: M, shard': M, step: Step)
   {