Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
9 changes: 9 additions & 0 deletions Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,15 @@ ragel:
lint:
golangci-lint run ./...

# Model-check the replication protocol spec (needs tla2tools.jar, see tla/README.md)
TLA2TOOLS ?= tla2tools.jar
.PHONY: tla
tla:
cd tla && for cfg in MCFixed MCFixedChurn MCFixedLast MCWitness MCPing MCBatchFixed MCBatchFixedLast; do \
echo "=== $$cfg ==="; \
java -XX:+UseParallelGC -cp $(TLA2TOOLS) tlc2.TLC -config $$cfg.cfg -workers auto -deadlock MCChotkiSync || true; \
done

.PHONY: update-pebble
update-pebble:
go mod edit -replace github.com/cockroachdb/pebble=github.com/drpcorg/pebble@master
Expand Down
4 changes: 4 additions & 0 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -79,6 +79,10 @@ Internally, Chotki is [pebble db][p] using [RDX](./rdx) merge operators.
See the RDX doc for further details on its serialization format
(type-length-value) and a very predictable choice of CRDTs.

The replication protocol is described in [replication](./replication)
and has a formal TLA+ specification in [tla](./tla), model-checked with
TLC (including reproductions of historical protocol bugs).

## Comparison to other projects

Overall, RDX is the final version of RON (Replicated Object
Expand Down
Loading
Loading