Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Rewrite PGo: simpler architecture, less code #140

Merged
merged 27 commits into from
Jul 29, 2021
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
27 commits
Select commit Hold shift + click to select a range
e800ba5
initial rewrite, WIP
fhackett Apr 21, 2021
36c7124
more manageable renaming; kind-matching semantic check; build.sbt
fhackett Apr 21, 2021
b525a3b
fix minor glitches; begin testing on real MPCal specs, normalize seem…
fhackett Apr 23, 2021
15f837f
WIP: read/write PCal tests, some progress on PCal codegen
fhackett May 4, 2021
4532a9f
WIP: fixed some pcal codegen bugs; tests still broken
fhackett May 6, 2021
6f72bdd
WIP: implement desugaring to single-variable assignment in pcalgen
fhackett May 7, 2021
aefedc8
WIP: pcalgen mode implementation almost-complete; missing MPCal proce…
fhackett May 7, 2021
7a4ac78
WIP: testing infrastructure; needs archetype resource implementations
fhackett Jun 1, 2021
a201f95
WIP: basic MVP network resources; dqueue tests pass
fhackett Jul 1, 2021
1b6b980
add comments to LocalArchetypeResource, run go fmt
fhackett Jul 1, 2021
1cc0dc9
WIP: fix bugs in kv_store spec compilation
fhackett Jul 5, 2021
a76041d
WIP: initial fuzz testing; implement Go operators; some resulting fixes
fhackett Jul 8, 2021
48014b4
WIP: reworking fuzz testing process
fhackett Jul 9, 2021
57167a1
WIP: AST coverage almost complete for fuzz testing; more bugs fixed
fhackett Jul 10, 2021
6ece9af
almost done fuzz testing; missing one node type
fhackett Jul 14, 2021
df91ea8
add fuzz testing for EXCEPT expression; fix related bugs
fhackett Jul 14, 2021
032de5e
add a couple of explanatory comments
fhackett Jul 15, 2021
876d004
Remove test reliance on empty paths that do not end up in the git repo.
fhackett Jul 15, 2021
a138d0e
Add multiple mapping macro error; make minor Go style changes.
fhackett Jul 17, 2021
2ce5330
Comment and clean up Go lib; add load_balancer test
fhackett Jul 23, 2021
2715174
add unsupported ops error; more clean-up
fhackett Jul 23, 2021
b4261d3
stub out replicated_kv Go test
fhackett Jul 23, 2021
fae2a7d
apply review recommendations; WARNING: slightly broken
fhackett Jul 24, 2021
e0e5085
Harden tests; fix bugs in channel and TCP resources
fhackett Jul 27, 2021
44da44d
Document invariants followed in tcpmailboxes.go
fhackett Jul 27, 2021
e7c552a
Implement more review recommendations
fhackett Jul 28, 2021
e6b891b
Even more review comments; fix broken case for .String() of an empty …
fhackett Jul 28, 2021
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
The table of contents is too big for display.
Diff view
Diff view
  •  
  •  
  •  
6 changes: 6 additions & 0 deletions .gitignore
Original file line number Diff line number Diff line change
Expand Up @@ -363,3 +363,9 @@ lib/pgo.jar

# ignore copied src in example/output/
/examples/output/*/src/

# Scala and sbt-related items
target/
project/
.bloop/
.bsp/
14 changes: 0 additions & 14 deletions .travis.yml

This file was deleted.

17 changes: 8 additions & 9 deletions build.sbt
Original file line number Diff line number Diff line change
@@ -1,21 +1,20 @@
name := "pgo"
scalaVersion := "2.13.4"
scalaVersion := "2.13.5"
javacOptions ++= Seq("-source", "1.8")

Compile / javaSource := baseDirectory.value / "src"
Test / javaSource := baseDirectory.value / "test"
Compile / scalaSource := baseDirectory.value / "src"
Test / scalaSource := baseDirectory.value / "test"

unmanagedJars in Compile ++= Seq(
file("lib/json.jar"),
file("lib/plume.jar"))
libraryDependencies += "org.scala-lang" % "scala-reflect" % scalaVersion.value

libraryDependencies += "org.scala-lang.modules" %% "scala-parser-combinators" % "1.2.0-M1"

libraryDependencies += "com.novocode" % "junit-interface" % "0.11" % Test
libraryDependencies += "org.rogach" %% "scallop" % "4.0.2"
libraryDependencies += "io.spray" %% "spray-json" % "1.3.6"

libraryDependencies += "org.scalatest" %% "scalatest" % "3.2.2" % Test
libraryDependencies += "org.scalatestplus" %% "junit-4-13" % "3.2.2.0" % Test
libraryDependencies += "org.scala-lang.modules" %% "scala-parser-combinators" % "1.2.0-M1"
libraryDependencies += "com.lihaoyi" %% "os-lib" % "0.7.3"

libraryDependencies += "org.scalatest" %% "scalatest" % "3.2.9" % Test
libraryDependencies += "org.scalatestplus" %% "scalacheck-1-15" % "3.2.9.0" % Test
libraryDependencies += "io.github.java-diff-utils" % "java-diff-utils" % "4.9" % Test
Binary file removed dev-lib/hamcrest-all-1.3.jar
Binary file not shown.
Binary file removed dev-lib/junit-4.12.jar
Binary file not shown.
116 changes: 116 additions & 0 deletions distsys/archetyperesource.go
Original file line number Diff line number Diff line change
@@ -0,0 +1,116 @@
package distsys

import (
"errors"
)

// ArchetypeResource represents an interface between an MPCal model and some external environment.
// Such a resource should be instantiated under the control of MPCalContext.EnsureArchetypeResourceByName or
// MPCalContext.EnsureArchetypeResourceByPosition. Typically, the former would be clearer.
// Many implementations are available under ./resources.
// This API describes what is expected of those implementations, and any others.
type ArchetypeResource interface {
// Abort will be called when the resource should be reset to a state similar to the last Commit.
// May return nil. If it doesn't return nil, the channel should notify one time, when the operation is complete.
// If it returns nil, the operation is considered complete immediately.
Abort() chan struct{}
// PreCommit will be called after any number of ReadValue, WriteValue, or Index operations.
// It signals if it is reasonable to go ahead with a Commit.
// If the resource might need to back out, it should do it here.
// May return nil. If it doesn't return nil, the channel should yield one error value. If the error is nil,
// Commit may go ahead. Otherwise, it may not.
// Returning nil is considered a short-cut to immediately yielding a nil error.
PreCommit() chan error
// Commit will be called if no sibling PreCommit calls raised any errors.
// It must unconditionally commit current resource state. By necessity, this is the only resource operation that
// may block indefinitely.
// May return nil. If it doesn't return nil, the channel should notify once the commit is complete.
// Returning nil is considered as an immediately successful commit.
Commit() chan struct{}
// ReadValue must return the resource's current value.
// If the resource is not ready, ErrCriticalSectionAborted may be returned alongside a default TLAValue.
// This operation should not block indefinitely.
// This makes no sense for a map-like resource, and should be blocked off with ArchetypeResourceMapMixin in that case.
ReadValue() (TLAValue, error)
// WriteValue must update the resource's current value.
// It follows the same conventions as ReadValue.
WriteValue(value TLAValue) error
// Index must return the resource's sub-resource at the given index.
// It's unclear when this would be needed, but, if the resource is not ready, then this operation may return
// ErrCriticalSectionAborted.
// This makes no sense for a value-like resource, and should be blocked off with ArchetypeResourceLeafMixin in that case.
Index(index TLAValue) (ArchetypeResource, error)
}

type ArchetypeResourceLeafMixin struct{}

var ErrArchetypeResourceLeafIndexed = errors.New("internal error: attempted to index a leaf archetype resource")

func (ArchetypeResourceLeafMixin) Index(TLAValue) (ArchetypeResource, error) {
return nil, ErrArchetypeResourceLeafIndexed
}

type ArchetypeResourceMapMixin struct{}

var ErrArchetypeResourceMapReadWrite = errors.New("internal error: attempted to read/write a map archetype resource")

func (ArchetypeResourceMapMixin) ReadValue() (TLAValue, error) {
return TLAValue{}, ErrArchetypeResourceMapReadWrite
}

func (ArchetypeResourceMapMixin) WriteValue(TLAValue) error {
return ErrArchetypeResourceMapReadWrite
}

// A bare-bones resource: just holds and buffers a TLAValue
// --------------------------------------------------------

type LocalArchetypeResource struct {
ArchetypeResourceLeafMixin
hasOldValue bool // if true, this resource has already been written in this critical section
// if this resource is already written in this critical section, oldValue contains prev value
// value always contains the "current" value
value, oldValue TLAValue
}

var _ ArchetypeResource = &LocalArchetypeResource{}
shayanh marked this conversation as resolved.
Show resolved Hide resolved

func LocalArchetypeResourceMaker(value TLAValue) ArchetypeResourceMaker {
return ArchetypeResourceMakerFn(func() ArchetypeResource {
return &LocalArchetypeResource{
value: value,
}
})
}

func (res *LocalArchetypeResource) Abort() chan struct{} {
if res.hasOldValue {
res.value = res.oldValue
res.hasOldValue = false
res.oldValue = TLAValue{}
}
return nil
}

func (res *LocalArchetypeResource) PreCommit() chan error {
return nil
}

func (res *LocalArchetypeResource) Commit() chan struct{} {
res.hasOldValue = false
res.oldValue = TLAValue{}
return nil
}

func (res *LocalArchetypeResource) ReadValue() (TLAValue, error) {
return res.value, nil
}

func (res *LocalArchetypeResource) WriteValue(value TLAValue) error {
if !res.hasOldValue {
res.oldValue = res.value
res.hasOldValue = true
}
res.value = value
return nil
}
5 changes: 5 additions & 0 deletions distsys/go.mod
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
module github.com/UBC-NSS/pgo/distsys

go 1.14

require github.com/benbjohnson/immutable v0.3.0
2 changes: 2 additions & 0 deletions distsys/go.sum
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
github.com/benbjohnson/immutable v0.3.0 h1:TVRhuZx2wG9SZ0LRdqlbs9S5BZ6Y24hJEHTCgWHZEIw=
github.com/benbjohnson/immutable v0.3.0/go.mod h1:uc6OHo6PN2++n98KHLxW8ef4W42ylHiQSENghE1ezxI=
Loading