Merge remote-tracking branch 'origin/async'

Author: tchajed

examples_test.go

@@ -183,6 +183,10 @@ func TestWal(t *testing.T) {
 	testExample(t, "wal", goose.Translator{TypeCheck: true})
 }
 
+func TestAsync(t *testing.T) {
+	testExample(t, "async", goose.Translator{TypeCheck: false})
+}
+
 func TestLogging2(t *testing.T) {
 	testExample(t, "logging2", goose.Translator{TypeCheck: true})
 }

goose.go

@@ -85,6 +85,11 @@ func getFfi(pkg *packages.Package) string {
 	seenFfis := make(map[string]struct{})
 	packages.Visit([]*packages.Package{pkg},
 		func(pkg *packages.Package) bool {
+			// the dependencies of an FFI are not considered as being used; this
+			// allows one FFI to be built on top of another
+			if _, ok := ffiMapping[pkg.PkgPath]; ok {
+				return false
+			}
 			return true
 		},
 		func(pkg *packages.Package) {
@@ -1859,19 +1864,21 @@ func stringLitValue(lit *ast.BasicLit) string {
 
 // TODO: put this in another file
 var builtinImports = map[string]bool{
-	"github.com/tchajed/goose/machine":         true,
-	"github.com/tchajed/goose/machine/filesys": true,
-	"github.com/mit-pdos/gokv/grove_ffi":       true,
-	"github.com/tchajed/goose/machine/disk":    true,
-	"github.com/mit-pdos/gokv/time":            true,
-	"sync":                                     true,
-	"log":                                      true,
-	"fmt":                                      true,
+	"github.com/tchajed/goose/machine":            true,
+	"github.com/tchajed/goose/machine/filesys":    true,
+	"github.com/mit-pdos/gokv/grove_ffi":          true,
+	"github.com/tchajed/goose/machine/disk":       true,
+	"github.com/tchajed/goose/machine/async_disk": true,
+	"github.com/mit-pdos/gokv/time":               true,
+	"sync":                                        true,
+	"log":                                         true,
+	"fmt":                                         true,
 }
 
 var ffiMapping = map[string]string{
-	"github.com/mit-pdos/gokv/grove_ffi":    "grove",
-	"github.com/tchajed/goose/machine/disk": "disk",
+	"github.com/mit-pdos/gokv/grove_ffi":          "grove",
+	"github.com/tchajed/goose/machine/disk":       "disk",
+	"github.com/tchajed/goose/machine/async_disk": "async_disk",
 }
 
 func (ctx Ctx) imports(d []ast.Spec) []coq.Decl {

internal/examples/async/async.go

@@ -0,0 +1,12 @@
+// async just uses the async disk FFI
+package async
+
+import "github.com/tchajed/goose/machine/async_disk"
+
+func TakesDisk(d async_disk.Disk) {}
+
+func UseDisk(d async_disk.Disk) {
+	v := make([]byte, 4096)
+	d.Write(0, v)
+	d.Barrier()
+}

internal/examples/async/async.gold.v

@@ -0,0 +1,16 @@
+(* autogenerated from github.com/tchajed/goose/internal/examples/async *)
+From Perennial.goose_lang Require Import prelude.
+From Perennial.goose_lang Require Import ffi.async_disk_prelude.
+
+(* async just uses the async disk FFI *)
+
+Definition TakesDisk: val :=
+  rec: "TakesDisk" "d" :=
+    #().
+
+Definition UseDisk: val :=
+  rec: "UseDisk" "d" :=
+    let: "v" := NewSlice byteT #4096 in
+    disk.Write #0 "v";;
+    disk.Barrier #();;
+    #().

machine/async_disk/async_disk.go

@@ -0,0 +1,16 @@
+package async_disk
+
+import (
+	"github.com/tchajed/goose/machine/disk"
+)
+
+// Essentially a copy + paste of the disk interface. We do this so that we can
+// change what Goose translate client code to (either the Disk FFI model or
+// Async Disk FFI model) based on which package is used.
+
+// Block is a 4096-byte buffer
+type Block = disk.Block
+
+const BlockSize uint64 = disk.BlockSize
+
+type Disk = disk.Disk

machine/async_disk/file.go

@@ -0,0 +1,13 @@
+package async_disk
+
+import (
+	"github.com/tchajed/goose/machine/disk"
+)
+
+type FileDisk = disk.FileDisk
+
+func NewFileDisk(path string, numBlocks uint64) (FileDisk, error) {
+	return disk.NewFileDisk(path, numBlocks)
+}
+
+var _ Disk = FileDisk{}

machine/async_disk/mem.go

@@ -0,0 +1,13 @@
+package async_disk
+
+import (
+	"github.com/tchajed/goose/machine/disk"
+)
+
+type MemDisk = disk.MemDisk
+
+func NewMemDisk(numBlocks uint64) MemDisk {
+	return MemDisk(disk.NewMemDisk(numBlocks))
+}
+
+var _ Disk = MemDisk{}