From 07fa0678eef998081c39a2a505ed8dadb4ef482c Mon Sep 17 00:00:00 2001 From: Federico Ponzi Date: Wed, 12 Jun 2024 18:11:09 +0100 Subject: [PATCH] structure draft --- src/SUMMARY.md | 18 ++++- src/chapter_1.md | 1 - src/codebase/architecture.md | 124 +++++++++++++++++++++++++++++ src/codebase/contributing.md | 72 +++++++++++++++++ src/codebase/ide.md | 1 + src/codebase/idiosyncrasies.md | 137 +++++++++++++++++++++++++++++++++ src/codebase/intro.md | 4 + src/codebase/wishlist.md | 82 ++++++++++++++++++++ src/community.md | 5 ++ src/intro.md | 3 + src/learning.md | 1 + 11 files changed, 446 insertions(+), 2 deletions(-) delete mode 100644 src/chapter_1.md create mode 100644 src/codebase/architecture.md create mode 100644 src/codebase/contributing.md create mode 100644 src/codebase/ide.md create mode 100644 src/codebase/idiosyncrasies.md create mode 100644 src/codebase/intro.md create mode 100644 src/codebase/wishlist.md create mode 100644 src/community.md create mode 100644 src/intro.md create mode 100644 src/learning.md diff --git a/src/SUMMARY.md b/src/SUMMARY.md index 7390c82..77a73b8 100644 --- a/src/SUMMARY.md +++ b/src/SUMMARY.md @@ -1,3 +1,19 @@ # Summary -- [Chapter 1](./chapter_1.md) +- [TLA+ Wiki intro](./intro.md) +- [TLA+ Codebase](./codebase/intro.md) + - [Contributing](./codebase/contributing.md) + - [Setting up the development environment](./codebase/ide.md) + - [Codebase Architecture Walkthrough](./codebase/architecture.md) + - [Codebase Idiosyncrasies](./codebase/idiosyncrasies.md) + - [Wishlist](./codebase/wishlist.md) + - [Tree-sitter grammar]() +- [Learning TLA+]() + - [Lamport's video tutorial]() + - [Example repo]() + - [Notable repos]() +- [Using TLA+]() + - [Standard Library]() + - [Community Modules]() +- [TLA+ Community: what to do when you're stuck](community.md) +- [TLAF: TLA+ Foundation]() diff --git a/src/chapter_1.md b/src/chapter_1.md deleted file mode 100644 index b743fda..0000000 --- a/src/chapter_1.md +++ /dev/null @@ -1 +0,0 @@ -# Chapter 1 diff --git a/src/codebase/architecture.md b/src/codebase/architecture.md new file mode 100644 index 0000000..7c6f994 --- /dev/null +++ b/src/codebase/architecture.md @@ -0,0 +1,124 @@ +# Codebase Architecture Walkthrough +### Modules +- [pcal](../src/pcal): Converts the pcal language into TLA+ that can by run by TLC2. +- [tla2tex](../src/tla2tex): "Pretty Prints" TLA+ code into LaTex. This LaTex can then be used for publishing. +- [tla2sany](../src/tla2sany): Contains the AST and parsing logic for the TLA+ language. The AST classes generated from parsing are used by TLC2. +- [tlc2](../src/tlc2): The model checker to validate the AST generated by tla2sany. This is the largest and most complex part of the codebase by far. + +### The Standard Flow +This is a generalized mplified description of how this code is normally used, and the involved components. More detail will be given on some of these components in the following sections. + +1. (Optional) PCal code translated into TLA+ code. [pcal.trans](src/pcal/trans.java)::main +2. TLC2 Model Checker run from standard entrypoint [tlc2.TLC](src/tlc2/TLC.java)::main on that code and associated .cfg file +3. TLC2 class created, arguments parsed, and processing started. [tlc2.TLC](src/tlc2/TLC.java)::TLC, TLC::handleParameters, TLC::process +4. The spec is parsed and stored in [Tool](../src/tlc2/tool/impl/Tool.java). This occurs in the Tool constructor. + 1. A [SpecObj](../src/tla2sany/modanalyzer/SpecObj.java) is created with file information about the spec + 2. A [SpecProcessor](../src/tlc2/tool/impl/SpecProcessor.java) is created with that SpecObj + 3. At the start of processing the spec, SpecProcessor calls [SANY](../src/tla2sany/drivers/SANY.java)::frontEndMain that parses the spec into an AST + 4. The SpecProcessor performs a number of extraction and analysis operations on the AST. + > Note: These are called in a precise order in the [Tool](../src/tlc2/tool/impl/Tool.java) constructor. Modifying this is highly error prone, though the tests will fail reliably if there is an issue. + 5. The Tool takes the results of all these operations and assigns them to final variables. The Tool is now the only source of truth for specification information, and is immutable. + > Note: This is a critical separation of concerns, to separate the complex job of parsing and resolving the spec, from the job of analyzing it. The tool is the only object that spans both. +5. The following are selected and initialized + - The model checker or simulator. This class performs a certain type of analysis on the spec. + - [ModelChecker](../src/tlc2/tool/ModelChecker.java): Standard Breadth-First checking of entire state space + - [FPSet](../src/tlc2/tool/fp/FPSet.java): Contains the fingerprints of all explored states. + - [StateQueue](../src/tlc2/tool/queue/IStateQueue.java): Contains new states to explore. + - [DFIDModelChecker](../src/tlc2/tool/DFIDModelChecker.java): Depth first checking of entire state space, to a pre-specified level of depth. + - [FPIntSet](../src/tlc2/tool/fp/dfid/FPIntSet.java) + - [Simulator](../src/tlc2/tool/Simulator.java): Randomized exploration and checking of the state space. +6. The analysis is performed + 1. Workers are run per configuration to allow multi-threaded analysis + - ModelChecker: [Worker](../src/tlc2/tool/Worker.java) + - DFIDModelChecker: [DFIDWorker](../src/tlc2/tool/DFIDWorker.java) + - Simulator: [SimulationWorker](../src/tlc2/tool/SimulationWorker.java) + 2. Each checker performs analysis differently, but generally the analysis consists of generating new states from existing states, and checking those new states +7. The result is returned to the user + +### Model Checker Analysis + +1. The StateQueue is seeded with the initial states +2. Workers take states of the StateQueue. From there they generate next potential states. They check that the fingerprint of the state is not already in the FPSet (such that analysis is not duplicated). They then check that state for safety properties, and add it to both the FPSet and the StateQueue.' +3. Periodically the analysis pauses. If configured to create a checkpoint, a checkpoint is created. If configured to check temporal properties, the Liveness Checking workflow (described below) is performed by calling [LiveChecker](../src/tlc2/tool/liveness/LiveCheck.java)::check. Once done the analysis continues. +4. When the StateQueue is empty or an error is detected, the analysis is over. + +> Performance Note: The vast majority of CPU cycles are spent either calculating fingerprints or storing fingerprints in the FPSet. + +### Depth-First Checker Analysis + +1. Data structure initialized with InitStates +2. The analysis occurs by setting a temporary max depth that increases to the configured maximum depth +3. Worker retrieves unexplored initial state, removing it from the set of init states +4. Worker explores the state space depth first up to the temporary max depth, storing all seen states in the FPIntSet +5. Periodically the analysis pauses. If configured to create a checkpoint, a checkpoint is created. If configured to check temporal properties, the Liveness Checking workflow (described below) is performed by calling [LiveCheck](../src/tlc2/tool/liveness/LiveCheck.java)::check. Once done the analysis continues. +6. Once there are no more levels to explore, or an error is detected, the analysis is over + + +### Simulator Analysis + +1. Initial states calculated and checked for validity +2. Each SimulationWorker retrieves a random initial state +3. Next states are randomly generated and checked, up to a specified depth. Each one of these runs is a trace. +4. If liveness checking is enabled, check the trace with [LiveChecker](../src/tlc2/tool/liveness/LiveCheck.java)::checkTrace +5. Once the specified number of traces have been run, or an error is detected, the analysis is over + +### Liveness Checking +Liveness checking is what allows checking of temporal properties. + +Liveness checking is initiated by calling: [LiveCheck](../src/tlc2/tool/liveness/LiveCheck.java)::check or checkTrace. + +Every time this occurs it creates new [LiveWorker](../src/tlc2/tool/liveness/LiveWorker.java)(s) to perform the analysis. + +> Note: Unlike standard model checking, Liveness Checking by default is not guaranteed to produce the shortest trace that violates the properties. There is a [AddAndCheckLiveCheck](../src/tlc2/tool/liveness/AddAndCheckLiveCheck.java) that extends LiveCheck that attempts to do this, at the cost of significant performance. It is selected in the constructor of [AbstractChecker](../src/tlc2/tool/AbstractChecker.java). + +### States and Fingerprints +States are a fundamental part of TLC. They represent a set of variable values, that entirely determine the state of the system. States are generated and checked as part of the TLC2 analysis process. The base class for this is [TLCState](../src/tlc2/tool/TLCState.java). + +Fingerprints are hashes taken of these states using the [FP64](src/tlc2/util/FP64.java) hash. Fingerprints are a 64bit hash representing the state. This is significantly smaller than storing the state itself, and yet collisions are very unlikely (though if they did occur, part of the statespace would not be explored). The fingerprinting process is initiated from [TLCState](../src/tlc2/tool/TLCState.java)::generateFingerPrint. + +There are two primary implementations of state that are very similar: +- [TLCStateMut](../src/tlc2/tool/TLCStateMut.java): Higher performance, records less information +- [TLCStateMutExt](../src/tlc2/tool/TLCStateMutExt.java): Lower performance, records more information + +Effectively, functions that are no-ops in TLCStateMut, persistently store that information in TLCStateMutExt. This information can include the name of the generating action, and is often needed for testing / debugging purposes. + +The implementation to use is selected in the constructor of [Tool](../src/tlc2/tool/impl/Tool.java), by setting a reference Empty state for the analysis. + +### High Performance Datastructures + +The ModelChecker performs a breadth-first search. In a standard BFS algorithm, there are two main datastructures: a queue of items of explore next, and a set of the nodes already explored. Because of the sheer size of the state space for the ModelChecker, specialized versions of these datastructures are used. + +> Note: These data-structures are a large focus of the profiling / testing work, because both performance and correctness are key for the ModelChecker to explore the full state space. + +#### Fingerprint Sets (FPSets) +FPSets are sets with two main operations +- put fingerprint +- determine if fingerprint in set + +Located in [tlc2.tool.fp](../src/tlc2/tool/fp). All but [FPIntSet](../src/tlc2/tool/fp/dfid/FPIntSet.java) extend [FPSet](../src/tlc2/tool/fp/FPSet.java). FPIntSet is used specifically for depth-first-search and is not discussed here. + +In practice the performance and size of the FPSet determine the extent of analysis possible. The [OffHeapDiskFPSet](../src/tlc2/tool/fp/OffHeapDiskFPSet.java) is in practice the most powerful of the FPSets, efficiently spanning the operations across off-heap memory and the disk. There are also memory only FPSets that may be preferable for smaller state spaces. + +#### StateQueue +Located in [tlc2.tool.queue](../src/tlc2/tool/queue), with all implementations extending [StateQueue](../src/tlc2/tool/queue/StateQueue.java). + +The default implementation is [DiskStateQueue](../src/tlc2/tool/queue/DiskStateQueue.java). Because of the size of the queue, storing it in memory may not be an option. + +### Symmetry Sets +A discussion of Symmetry Sets can be found [here](https://www.learntla.com/core/constants.html). + +They are implemented in the [TLCState](../src/tlc2/tool/TLCState.java)::generateFingerPrint function by calculated all permutations of a particular state (for all symmetry set model values), and returning the smallest fingerprint. Therefore all permutations would have a same fingerprint, and so only the first example generated would be explored. + +> Note: The order dependant nature of the fingerprint means that when using symmetry sets, the majority of the cpu cycles are spent "normalizing" the data structures such that the order the fingerprint gets assembled in are consistent. An order independent fingerprint hash would remove this performance hit, however would significantly increase the likelihood of collisions unless the hash algorithm itself was upgraded. + +### Debugger +The [AttachingDebugger](../src/tlc2/debug/AttachingDebugger.java) is the main debugger. It works in conjunction with the [DebugTool](../src/tlc2/tool/impl/DebugTool.java) to allow a user to step through a TLC execution. + +> Note: Using the debugger will keep the process alive indefinitely due to the listener. The eclipse network listener is not interruptable, so thread interruption behavior will not work. It relies on process exit. + +### Coverage +The coverage functionality determines what statements in the TLA+ spec have been used. +Located in [tlc2.tool.coverage](../src/tlc2/tool/coverage) + +### Unique Strings +String comparison can be a relatively expensive operation compared to primitive comparison. There are lots of string comparisons required in the code, but with a relatively limited set of strings.[UniqueString](../src/util/UniqueString.java) maps each string to a monotonically increasing integer. Then comparisons are reduced to the much cheaper integer comparisons. This is used throughout the codebase. \ No newline at end of file diff --git a/src/codebase/contributing.md b/src/codebase/contributing.md new file mode 100644 index 0000000..15fe512 --- /dev/null +++ b/src/codebase/contributing.md @@ -0,0 +1,72 @@ +# Contributing + +TL;DR: engage maintainers early & often, be surgical in your changes, and write lots of tests. + +We welcome contributions to this open source project! +Before beginning work, please take some time to familiarize yourself with our development processes and expectations. +The TLA⁺ tools are used to validate safety-critical systems, so maintaining quality is paramount. +The existing code can also be quite complicated to modify and it is difficult to review changes effectively. +So, there are several practices that are necessary for having a good contribution experience. +The last thing anybody wants is for you to feel as though you have wasted your time! +If you open a massive pull request (PR) out of nowhere it is **very unlikely to be merged**. +Follow this guide to ensure your effort is put to the best possible use. + +Always remember that we are all volunteers here. +Be kind to everybody! +You can review our Code of Conduct [here](.github/CODE_OF_CONDUCT.md). + +The Contribution Process & Style +-------------------------------- + +The most important step is to engage with existing developers & maintainers before beginning work. +The best way to do this is to comment on an issue you want to fix, or open a new issue if a suitable candidate does not exist. +It is also very helpful to join the [monthly online community meeting](https://groups.google.com/g/tlaplus/c/CpAEnrf-DHQ/m/YrORpIfSBwAJ) to introduce yourself and speak with people directly. +The development team will help you better understand the scope & difficulty of the proposed changes, along with what parts of the codebase they'll touch and what additional tests are required to safely merge them. +Building & maintaining consensus around these aspects will ensure a smooth review & merge process. + +To begin work on your change, fork this repository then create an appropriately-named branch to track your work. +You will eventually submit a PR between your feature branch and the master branch of this repository, at which point developers & maintainers will review your changes. +After integrating this feedback your PR will then hopefully be merged. + +When creating and submitting your changes, closely follow these guidelines: + * **Be surgical:** What is the smallest diff you can make that still accomplishes your goal? + Avoid the urge to fix unrelated stylistic issues in a file you are changing. + * **Write tests first:** If you're changing a specific part of the codebase, first ensure it has good test coverage; if it does, write a few more tests yourself anyway! + Writing tests is a great way to learn how the code functions. + If possible, submit your tests in a separate PR so their benefits can be realized immediately. + We don't fully subscribe to Test-Driven Development (TDD) but having good existing test coverage of a changed area is a prerequisite to changes being merged. + * **Split up your changes:** If parts of your changes provide some benefit by themselves - like additional tests - split them into a separate PR. + It is preferable to have several small PRs merged quickly than one large PR that takes longer to review. + * **Craft your commits well:** This can require advanced git knowledge (see [DEVELOPING.md](DEVELOPING.md)). + Treat your commits as forms of communication, not a way to bludgeon the codebase into shape. + You don't need to check this, but ideally the build & tests should pass on every commit. + This means you will often be amending commits as you work instead of adding new ones. + +When you open a PR against this repo, the continuous integration (CI) checks will run. +These ensure your changes do not break the build & tests. +While you can run most of these checks locally, if you'd like to run the CI at any time you can open a PR between your feature branch and the master branch of *your own* fork of this repo. + +Contribution Possibilities +-------------------------- + +These tools have a large number existing issues to fix, which you can see on the repo's [issues tab](https://github.com/tlaplus/tlaplus/issues). +In particular, consider looking at issues [tagged with "help wanted"](https://github.com/tlaplus/tlaplus/issues?q=is%3Aopen+is%3Aissue+label%3A%22help+wanted%22). +For new developers, there are issues [tagged "good first issue"](https://github.com/tlaplus/tlaplus/labels/good%20first%20issue). + +For new features, there are a number of [substantial improvements we'd like to see implemented](general/docs/contributions.md). +If you have an idea for a new feature, open an issue in this repository to start a discussion. +For more fundamental proposals that involve changes to the TLA⁺ language itself, you can [open a RFC](https://github.com/tlaplus/rfcs/issues). +Often it will be necessary to build community support for your idea; for this you can use the [mailing list](https://groups.google.com/g/tlaplus) and especially the [monthly online community meeting](https://groups.google.com/g/tlaplus/c/CpAEnrf-DHQ/m/YrORpIfSBwAJ). +Expressions of goodwill like volunteering labor to review pending PRs is also appreciated! + +Non-code contributions are also welcome! +There is ample work available in expanding developer documentation (like this very document) or user-facing TLA⁺ documentation. +We also collect [quality metrics](https://sonarcloud.io/organizations/tlaplus/projects), and the reports indicate several low-hanging fruits to pick. + +Getting Started +--------------- + +Take the time to set up your local development environment. +See [DEVELOPING.md](DEVELOPING.md) for details. +Good luck, and have fun! + diff --git a/src/codebase/ide.md b/src/codebase/ide.md new file mode 100644 index 0000000..5088a5a --- /dev/null +++ b/src/codebase/ide.md @@ -0,0 +1 @@ +# Setting up the development environment diff --git a/src/codebase/idiosyncrasies.md b/src/codebase/idiosyncrasies.md new file mode 100644 index 0000000..19dcca9 --- /dev/null +++ b/src/codebase/idiosyncrasies.md @@ -0,0 +1,137 @@ +# Codebase Idiosyncrasies + +As a 20 year old code base, one can expect idiosyncrasies that do not match current best practice. There are also inherent idiosyncrasies to any language interpreter. Maintaining functionality and performance is the most important concern. However whenever these idiosyncrasies can be removed without compromising those, they should be. + +### Dynamic Class Loading +This project makes extensive use of Classloaders. This can make it slightly more difficult to debug / statically analyze. Critical usecases are called out here. + +#### Operators / Modules +The ClassLoader is used to load both standard modules and user created modules. The standard modules can be found here: +- [src/tlc2/module](../src/tlc2/module) +- [src/tla2sany/StandardModules](../src/tla2sany/StandardModules) + +The [SimpleFilenameToStream](../src/util/SimpleFilenameToStream.java) class is used to read in this information, and contains the logic about standard module directories. It is where the ClassLoader is used. [TLAClass](../src/tlc2/tool/impl/TLAClass.java) is also used for a similar purpose, used to loader certain built in classes. + +The classpath of the created jar explicitly includes the CommunityModules such that they can be loaded if available. +``` +CommunityModules-deps.jar CommunityModules.jar +``` + +Users can also create custom operators and modules and load them similarly. + +The methods are invoked with: +``` java +mh.invoke +mh.invokeExplict +``` + +And this is done in a small number of locations: +[MethodValue](../src/tlc2/value/impl/MethodValue.java) +[CallableValue](../src/tlc2/value/impl/CallableValue.java) +[PriorityEvaluatingValue](../src/tlc2/value/impl/PriorityEvaluatingValue.java) + + +#### FPSet Selection + +FPSets are dynamically selected using a system property and loaded with a ClassLoader in the [FPSetFactory](../src/tlc2/tool/fp/FPSetFactory.java). + +#### Misc +- [TLCWorker](../src/tlc2/tool/distributed/TLCWorker.java): Used to load certain sun class dependencies if available. +- [BlockSelectorFactory](../src/tlc2/tool/distributed/selector/BlockSelectorFactory.java): Used to modularity load a custom BlockSelectorFactory. +- [TLCRuntime](../src/util/TLCRuntime.java): Used to get processId + +### Notable Mutable Static State +The original codebase was written with the intention of being run from the command line only. + +There is a significant amount of static state. While much has been removed +- [util/UniqueString.java](../src/util/UniqueString.java): +- [util/ToolIO.java](../src/util/ToolIO.java): Used for +- [tlc2/TLCGlobals.java](../src/tlc2/TLCGlobals.java): + +### Testing Brittleness + +The end to end test suite is a very powerful tool of the project. It does have a reliance on the execution occurring in a very precise order. There are certain race conditions in the codebase that can cause some inconsistency in execution statistics, even while providing correct behavior. This can cause some tests to fail. Additionally, there are some race condition bugs. Additonally. It is not always easy to determine which case it falls into, and so categorizing / fixing these test cases should lead either codebase or test suite improvements. + +#### Independently Run Tests + +In order to allow tests to be independently run, we add one of the following tags depending on whether it is a standard test or a TTraceTest + +``` java +@Category(IndependentlyRunTest.class) +@Category(IndependentlyRunTTraceTest.class) +``` + +In general, these should be used sparingly, and instead if a test fails when run with others, the root cause should be discovered and fixed. + +#### Unique String ordering reliance + +As mentioned above, unique strings replace strings with a consistent integer token for faster comparison. That token is monotonically increasing from when the unique string is generated. When comparing unique strings, it compares the tokens, meaning the ordering of the UniqueString based collection is dependant on the ordering of the creation of strings. This can break tests that hardcode the ordering of the result output when they are not run in isolation. This isn't necessarily a fundamental problem with the system, as the output is consistent based on TLA+ semantics which does not differ based on order. + +The tests that fail for this reason are marked as independent tests, but grouped under + +``` xml +unique-string-conflicts +``` + +in [pom.xml](../pom.xml). Their reason for failure is known. + +#### Debugger Tests +The AttachedDebugger currently only terminates on process exit. For that reason, all debugger tests are marked with the annotation below, and run as independent processes. + +``` java +@Category(DebuggerTest.class) +``` + +### Primitive Versions of Standard Data Structures + +The standard collections in the Java standard library store only objects. Some custom collections are required that can store and/or be indexed by primitives. These are needed for performance reasons. +- [LongVec](../src/tlc2/util/LongVec.java) +- [IntStack](../src/tlc2/util/IntStack.java) +- [SetOfLong](../src/tlc2/util/SetOfLong.java) +- [ObjLongTable](../src/tlc2/util/ObjLongTable.java) +- [LongObjTable](../src/tlc2/util/LongObjTable.java) + +> Note: There may be more not listed here, but ideally they should be added. + +### Unchecked Casting +As a language interpreter, there are a number of Abstract Syntax Tree node types. In many cases, functions use unchecked casts to resolve these node types, often after using if statements to check the nodes type. + +To find all the classes / functions that do this, search for: +``` +@SuppressWarnings("unchecked") +``` + +Whenever possible unchecked casts should be replaced with [pattern matching instanceof](https://docs.oracle.com/en/java/javase/17/language/pattern-matching-instanceof-operator.html). This generally is a good fit for most of the code in the codebase. + +### Dead Code +This project was initiated prior to "good" version control. Therefore modern anti-patterns such as commenting out code and leaving unused methods, classes, etc have propagated. Significant amounts of dead code have been removed. Because of the use of reflection / classloaders, static analysis tools may indicate certain items are unused when they are actually depended on. Dead code removal needs to be done in conjunction with testing and exploration. + +#### Acceptable Dead Code +A certain amount of dead code may have explanatory purpose. +- Standard methods implemented on data structures: ideally they should be tested, but some are not. +- Semantic variables / properties that are set appropriately but unread: They serve as a form of comment. Misleading examples of these should be removed. +- Small amounts of inline, commented out code that changes particular functionality or configures the codebase. +- Tested classes that implement used interfaces, where the class is not currently used: These still have explanatory purpose. + +Any of this code should be removed when it loses relevance or accuracy. + +#### Dead Code to be Removed +- Commented out methods +- Orphan classes +- Large amounts of inline commented out code without sufficient explanatory power +- Unused, untested, non-standard methods: Version control can be used if they are needed, but they add confusion and may be broken + + +### Inconsistent Formatting +The formatting of certain classes is inconsistent and doesn't work well with modern IDEs. Ideally an autoformatter would be run on the codebase to fix this. However, as this is a fork of the primary codebase, it is left unrun to allow better diffs with the upstream repo. + +### JMX / Eclipse Integrations +This project was initially developed as an Eclipse project, so it includes a number of Eclipse libraries and technologies. Most of them integrate rather seamlessly as dependencies, while enabling specialized diagnostic functionality for Eclipse. + +The project has [AspectJ](https://en.wikipedia.org/wiki/AspectJ) source that can be compiled in for additional diagnostics. It is also required for Long Tests to pass. The sources are located in [src-aspectj](../src-aspectj). + +Additionally this project uses Java Management Extensions for diagnostic purposes. They are always used an can be a source of memory leaks. + + +### Java Pathfinder +There are java pathfinder tests in the project. Sources are located in [test-verify](../test-verify/). Additional information on these tests can be found in [test-verify/README](../test-verify/README.md). \ No newline at end of file diff --git a/src/codebase/intro.md b/src/codebase/intro.md new file mode 100644 index 0000000..4524b70 --- /dev/null +++ b/src/codebase/intro.md @@ -0,0 +1,4 @@ +# TLA+ codebase +The tlatools codebase is a complex one, there are over 600k lines of code, in over 2000 files, written over 20+ years. And yet as the best distributed systems modelling tool on the market today, maintaining and improving it is critical. + +This overview is meant to orient new programmers as well as reorient existing ones. \ No newline at end of file diff --git a/src/codebase/wishlist.md b/src/codebase/wishlist.md new file mode 100644 index 0000000..a64eac1 --- /dev/null +++ b/src/codebase/wishlist.md @@ -0,0 +1,82 @@ +# Wishlist: List of projects to extend/improve TLA+, TLC, TLAPS or the Toolbox + +Please also consult the [issues tracker](https://github.com/tlaplus/tlaplus/issues) if you want to get started with contributing to TLA+. The items listed here likely fall in the range of man-months. + +TLC model checker +----------------- +#### ([In Progress](https://bitbucket.org/parvmor/tarjanconcurrentscc/)) Concurrent search for strongly connected components (difficulty: high) (skills: Java, TLA+) +One part of TLC's procedure to check liveness properties, is to find the liveness graph's [strongly connected components](https://en.wikipedia.org/wiki/Strongly_connected_component) (SCC). TLC's implementation uses [Tarjan's](https://en.wikipedia.org/wiki/Strongly_connected_component) canonical solution to this problem. Tarjan's algorithm is a sequential algorithm that runs in linear time. While the time complexity is acceptable, its sequential nature causes TLC's liveness checking not to scale. Recently, concurrent variants of the algorithm have been proposed and studied in the scope of other model checkers ([Multi-Core On-The-Fly SCC Decomposition](https://github.com/utwente-fmt/ppopp16) & [Concurrent On-the-Fly SCC Detection for Automata-Based Model Checking with Fairness Assumption](http://ieeexplore.ieee.org/document/7816578/)). This work will require writing a TLA+ specification and ideally a formal proof of the algorithm's correctness. + +#### Liveness checking under symmetry (difficulty: high) (skills: Java, TLA+) +[Symmetry reduction](http://www.cs.cmu.edu/~emc/papers/Conference%20Papers/Symmetry%20Reductions%20in%20Model%20Checking.pdf) techniques can significantly reduce the size of the state graph generated and checked by TLC. For safety checking, symmetry reduction is well studied and has long been implemented in TLC. TLC's liveness checking procedure however, can fail to find property violations if symmetry is declared. Yet, there is no reason why symmetry reduction cannot be applied to liveness checking. This work will require writing a TLA+ specification and ideally a formal proof of the algorithm's correctness. + +#### TLC error reporting 2.0 (difficulty: moderate) (skills: Java) +TLC can only check a subset of TLA+ specifications. This subset is left implicit and a user might use language constructs and/or models that cause TLC to fail. Not infrequently, it comes up with the very helpful report “null”. To lower to barrier to learning TLA+, TLC error reporting has to better guide a user. + +#### Improved runtime API for TLC (difficulty: moderate) (skills: Java) +The TLC process can be long running. It possibly runs for days, weeks or months. Today, the Toolbox interfaces with the TLC process via the command line. The Toolbox parses TLC's output and visualizes it in its UI. This is a brittle and read-only interface. Instead, communication should be done via a bidirectional network API such as RMI, JMX or REST. A network interface would even allow users to inspect and control remotely running TLC instances, e.g. those running in the cloud started through [cloud-based distributed TLC](https://tla.msr-inria.inria.fr/tlatoolbox/doc/cloudtlc/index.html). A network interface is likely to require some sort of persistence mechanism to store model runs. Persistence of model runs is trivially possible with today's text based solution. Desirable user stories are: + - Pause/Resume TLC + - Reduce/Increase number workers + - Trigger checkpoints and gracefully terminate + - Trigger liveness checking + - Inspection hatch to see states currently being generated + - Metrics overall and for fingerprint set, state queue, trace + - ... + + +TLAPS +----- +#### Automatic expansion of operator definitions (difficulty: moderate) (skills: OCaml) + +TLAPS currently relies on the user to indicate which operator definitions should be expanded before calling the back-end provers. Forgetting to expand an operator may make an obligation unprovable, expanding too many operators may result in a search space too big for the back-end to handle. The objective of this work would be to automatically detect which definitions have to be expanded, based on iterative deepening and possibly heuristics on the occurrences of operators in the context. The method could return the list of expanded operators so that it can be inserted in the proof, eschewing the need for repeating the search when the proof is rerun. Doing so requires modifying the proof manager but not the individual back-end interfaces. + +#### SMT support for reasoning about regular expressions (difficulty: moderate to high) (skills: OCaml, SMT, TLA+) + +Reasoning about TLA+ sequences currently mainly relies on the lemmas provided in the module SequenceTheorems and therefore comes with very little automation. Certain SMT solvers including [Z3](https://sites.google.com/site/z3strsolver/) and [CVC4](https://github.com/CVC4/CVC4) include support for reasoning about strings and regular expressions. Integrating these capabilities in TLAPS would be useful, for example when reasoning about the contents of message channels in distributed algorithms. Doing so will require extending the SMT backend of TLAPS, including its underlying type checker for recognizing regular expressions, represented using custom TLA+ operators. + +#### Generate counter-examples for invalid proof obligations (difficulty: moderate to high) (skills: OCaml, TLA+) + +Most conjectures that users attempt to prove during proof development are in fact not valid. For example, hypotheses needed to prove a step are not provided to the prover, the invariant may not be strong enough etc. When this is the case, the back-end provers time out but do not provide any useful information to the user. The objective of this work is to connect a model generator such as [Nunchaku](https://github.com/nunchaku-inria/nunchaku) to TLAPS that could provide an explanation to the user why the proof obligation is not valid. The main difficulty will be defining a translation from a useful sublanguage of TLA+ set-theoretic expressions to the input language of Nunchaku, which resembles a functional programming language. + +#### Warning about unexpanded definitions (difficulty: moderate) (skills: OCaml, TLA+) + +A common reason for a proof not to succeed is the failure to tell the prover to expand a definition that needs to be expanded (see section 6.1 of [Proving Safety Properties](https://lamport.azurewebsites.net/tla/proving-safety.pdf) for an example). In some cases, simple heuristics could indicate that a definition needs to be expanded--for example, if a goal contains a symbol that does not appear in any formula being used to prove it. The objective is to find and implement such heuristics in a command that the user can invoke to suggest what definitions may need to be expanded. We believe that this would be an easy way to save users a lot of--especially beginning users. + +TLA Toolbox +----------- +#### Port Toolbox to e4 (difficulty: easy) (skills: Java, Eclipse) +[e4](http://www.vogella.com/tutorials/EclipseRCP/article.html) represents the newest programming model for Eclipse RCP applications. e4 provides higher flexibility while simultaneously reducing boilerplate code. The TLA Toolbox has been implemented on top of Eclipse RCP 3.x and thus is more complex than it has to. + +#### Add support for Google Compute to Cloud TLC (difficulty: easy) (skills: jclouds, Linux) +The Toolbox can launch Azure and Amazon EC2 instances to run model checking in the cloud. The Toolbox interfaces with clouds via the [jclouds](https://jclouds.apache.org/) toolkit. jclouds has support for Google Compute, but https://github.com/tlaplus/tlaplus/blob/master/org.lamport.tla.toolbox.jclouds/src/org/lamport/tla/toolbox/jcloud/CloudDistributedTLCJob.java has to be enhanced to support Google Compute. + +#### Add support for x1 instances to jclouds (difficulty: easy) (skills: jclouds) +We raised an [enhancement request for the jclouds toolkit](https://issues.apache.org/jira/browse/JCLOUDS-1339) to add support for Amazon's largest compute instances [(x1e.32xlarge, x1.32xlarge, x1.16xlarge)](https://aws.amazon.com/ec2/instance-types/x1/). + +#### Finish Unicode support (difficulty: easy) (skills: Eclipse, SANY) +A few [outstanding issues](https://github.com/tlaplus/tlaplus/issues?q=is%3Aissue+is%3Aopen+label%3AUnicode) prevent the integration of the Unicode support into the Toolbox. In addition to the open issues, adding unit tests would be welcomed. A [nightly/ci Jenkins build](https://tla.msr-inria.inria.fr/build/job/M-HEAD-pron-unicode-Toolbox.product.standalone/) is available. + +TLA+ Tools +---------- +#### Pretty Print to HTML (difficulty: easy) (skills: Java, HTML) +TLA+ has a great pretty-printer to TeX (`tla2tex`), but HTML is becoming a de-facto document standard, especially for content shared online. HTML also has other advantages, such as the ability to automatically add hyperlinks from symbols to their definitions, and allow for collapsing and expanding proofs. The existing `tla2tex` code already contains most of the necessary parsing and typesetting pre-processing (like alignment), and could serve as a basis for an HTML pretty-printer. A [prototype already exists](https://github.com/tlaplus/tlaplus/issues/146). + +Documentation and Code Quality +------------------------------ +The TLA+ source code was written by multiple people over many years, so it has cosmetic problems that are distracting to new contributors. **In general, we are not interested in cosmetic or stylistic improvements unless they also fix a concrete issue.** Large refactors carry a big risk of introducing new defects, and we have rejected well-intentioned refactors in the past because they are too large or risky to review. + +However, we are happy to accept small, easy-to-review changes that incrementally improve the TLA+ toolbox and tools. Below are a few meaningful ways to improve TLA+'s documentation and code quality. + +#### Improve Internal Documentation (difficulty: easy) (skills: technical writing) +The TLA+ [internal documentation for developers](https://github.com/tlaplus/tlaplus/blob/master/DEVELOPING.md) is limited. Improving this documentation would make it much easier for new contributors to get started. + +#### Improve Test Coverage (difficulty: moderate) (skills: Java) +While the TLA+ tools have good test coverage, we would much prefer them to have _great_ test coverage. This is a low-risk activity that any developer can help with. + +#### Remove Uses of Global Mutable Variables (difficulty: high) (skills: Java) (low priority) +TLC cannot be easily used as a library in other projects because it makes extensive use of global mutable variables. This is not a problem for the normal use case; TLC has always been intended to run as an isolated process, not as a library. Using a separate process is a deliberate choice and a strength: the operating system provides isolation in case TLC runs out of memory and crashes. However, there would be real benefits to allowing TLC to be used as a library, e.g. [reducing test suite execution time](https://github.com/tlaplus/tlaplus/pull/756). + +Fixing the existing uses of global variables must be undertaken carefully and incrementally. Previous efforts to do it have resulted in subtle soundness and completeness bugs. + +#### Replace Custom Data Structures with Standard Java Collections (difficulty: moderate) (skills: Java) (low priority) +The TLA+ tools have handwritten implementations of many now-standard collection classes, such as `tla2sany.utilities.Vector` and `tlc2.util.Vect`, which duplicate the functionality of `java.util.ArrayList`. Replacing the handwritten ones with the standard types would have multiple benefits, including reducing our maintenance burden, reducing the size of the compiled tools JAR, and eliminating latent bugs. Note however that there are [subtle differences](https://github.com/tlaplus/tlaplus/pull/328#issuecomment-542160722) between the handwritten implementations and the standard ones that must be accounted for. diff --git a/src/community.md b/src/community.md new file mode 100644 index 0000000..6a19db2 --- /dev/null +++ b/src/community.md @@ -0,0 +1,5 @@ +# TLA+ Community: what to do when you're stuck +* google group +* reddit +* stackoverflow +* community meetings diff --git a/src/intro.md b/src/intro.md new file mode 100644 index 0000000..5cc5e5b --- /dev/null +++ b/src/intro.md @@ -0,0 +1,3 @@ +# TLA+ Wiki intro +Welcome to TLA+ wiki. If you find errors, or have suggestions or feedback, please create a PR or an issue. + diff --git a/src/learning.md b/src/learning.md new file mode 100644 index 0000000..ffdb276 --- /dev/null +++ b/src/learning.md @@ -0,0 +1 @@ +# Learning TLA+