apple / swift-distributed-actors

Peer-to-peer cluster implementation for Swift Distributed Actors
https://apple.github.io/swift-distributed-actors/
Apache License 2.0
597 stars 56 forks source link

Model the membership merges using TLA+ #407

Open ktoso opened 4 years ago

ktoso commented 4 years ago

Would be nice to model the merge formally, to sanity check we're not missing any edge case.

The merges are generally simple, except for removal which involves some special handling.

ktoso commented 4 years ago

See https://github.com/apple/swift-distributed-actors/tree/master/Models for other model examples