1-Update is a new cache coherence protocol that is based on traditional invalidate protocols and also adopts the advantages of updating protocols. It tracks the number of writes to a shared block, and sends at most one update to the reader cores after the observed number of writes. A brief description follows and more details can be found in the PACT'21 paper.
This is the publicly available artifact repository supporting 1-Update, which contains the formal protocol specification. The specification is written in TLA+ and can be used to verify 1-Update's correctness via model-checking.
- The 1-Update specification is decoupled into two modules folder for simplicity. OneUpdate.tla and OneUpdateMeta.tla.
To model check 1-Update, you need to download and install the TLA+ Toolbox so that you can run the TLC model checker using the TLA+ specification. We next list the steps for model checking.
- Prerequisites: Any OS with Java 1.8 or later, to accommodate the TLA+ Toolbox.
- Download and install the TLA+ Toolbox.
- Launch the TLA+ Toolbox.
- Create a spec: File>Open Spec>Add New Spec...; Browse and use 1Update/OneUpdate.tla as root module to finish.
- Create a new Model: Navigate to TLC Model Checker>New model...; and create a model with the name "one-update-model".
- Setup Behavior: In Model Overview tab of the model, and under the "What is the behavior spec?" section, select "Temporal formula" and write "Spec".
- Setup Constants: Then specify the values of declared constants (under "What is the model?" section). You may use low values for constants to check correctness without exploding the state space. An example configuration would be four cores, maximum writes of seven and an update prediction of 3. To accomplish that, you would need to click on each constant and select the "ordinary assignment" option. Then fill the box for write related constants (i.e., MAX_WRITES and WRITE_TO_UPDATE) with the desired number (e.g., with "7" and "5") and the core related constant (i.e., CORES) with a set of cores (e.g., "{1,2,3,4}" -- for four cores). Finally, to model check the variant of thepaper where the acknowledgments are gathered by the directory instead of the writer set the ENABLE_DIR_ACKS to TRUE.
This work is freely distributed under the Apache 2.0 License.