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

Conversation

fhackett
Copy link
Contributor

@fhackett fhackett commented Jul 1, 2021

A significant blocker for working on PGo has been a bulky, hard to understand codebase.

This PR is the almost-conclusion to a near-complete rewrite of the compiler and most of its runtime libraries.
The codebase becomes pure Scala (and Go), loses >20k LOC, and is written in a much more agile and mostly-declarative style.
The Go codebase gains module support.

This does not come without a cost: some legacy modes have been removed.

Overall changes:

  • PGo no longer even attempts type inference, instead using a dynamically-typed data model, which is simpler, and more closely emulates TLA+ semantics.
  • The TLA+ data model is represented more efficiently, using immutability-optimised data structures similar to those in the Scala stdlib
  • PCal (as opposed to MPCal) compilation mode is removed for MVP. It was not very useful; though it would not be hard to add it back.
  • Most operations are expressed as function calls to generalised Go code, allowing the majority of complex code to be tested, debugged, etc using standard Go tooling.
  • The critical section model is currently under redesign. TODO: finish this
  • A new testing setup inspired by the Viper / Dotty setups allows most user-level tests to be written in annotated MPCal and Go, by placing specially named files in the test folder.

This PR is more or less ready for feedback, but lacks documentation and testing. These will come.

@fhackett
Copy link
Contributor Author

Some progress notes: this rewrite now has fuzz-tested coverage of all recognised value-level TLA+ AST types and a large majority of built-in operations.

The design of the archetype resource / context / critical section system Go-side still needs work.
The current draft API for persistence does not properly account for off-thread writes to resources (e.g when a mailbox receives a message, it is added async).

At a high level, my idea for fixing this issue is to implement async writes using a model similar to flat-combining, with durability coming from a form of write-ahead logging + async compaction. This would likely be much more efficient than my current idea, might also work well with current ideas on PGo output validation (via the logging part).

For now, though, I'm seriously considering just scrapping the durability API entirely for the MVP, as it's a lot of trouble, and it would be massive scope creep to actually work through and validate the different design ideas. Turns out it's not just a "let's pin an API on it and get it right later" problem...

Note: the failing checks are because of two known-failing examples. This is more or less because the tests have not properly been written / worked through yet, which should be done before merging.

distsys/archetype_resources/channels.go Outdated Show resolved Hide resolved
distsys/mpcal_context.go Outdated Show resolved Hide resolved
distsys/archetype_resources/tcp_mailboxes.go Outdated Show resolved Hide resolved
distsys/mpcal_context.go Outdated Show resolved Hide resolved
distsys/mpcal_context.go Outdated Show resolved Hide resolved
distsys/mpcal_context.go Outdated Show resolved Hide resolved
distsys/archetype_resources/tcp_mailboxes.go Outdated Show resolved Hide resolved
distsys/archetype_resources/tcp_mailboxes.go Outdated Show resolved Hide resolved
distsys/resources/tcpmailboxes.go Outdated Show resolved Hide resolved
distsys/resources/tcpmailboxes.go Outdated Show resolved Hide resolved
distsys/resources/incrementalmap.go Outdated Show resolved Hide resolved
distsys/resources/incrementalmap.go Outdated Show resolved Hide resolved
distsys/resources/tcpmailboxes.go Show resolved Hide resolved
distsys/resources/tcpmailboxes.go Outdated Show resolved Hide resolved
distsys/resources/tcpmailboxes.go Outdated Show resolved Hide resolved
distsys/resources/tcpmailboxes.go Outdated Show resolved Hide resolved
distsys/resources/tcpmailboxes.go Show resolved Hide resolved
distsys/resources/tcpmailboxes.go Show resolved Hide resolved
distsys/archetyperesource.go Show resolved Hide resolved
distsys/resources/tcpmailboxes.go Outdated Show resolved Hide resolved
distsys/resources/channels.go Outdated Show resolved Hide resolved
distsys/resources/filesystem.go Show resolved Hide resolved
distsys/resources/tcpmailboxes.go Show resolved Hide resolved
@shayanh shayanh merged commit 35a455d into master Jul 29, 2021
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Rewriting Go code gen PGo rewrite: Go-land data model implementation
2 participants