/cure-kvstore-tla

TLA+ Spec for the Cure Key-Value Store

Primary LanguageTeXMIT LicenseMIT

cure-kvstore-tla

TLA+ Spec for the Cure Key-Value Store

Design Choices for TLA+ Spec

  • Data Sharding
    • Sharding is a mapping from Key to Partition
      1. Random mapping in each model checking (not CHOOSE; try RandomElement)
      2. As a part of model
  • Clock[p][d]
    • Tick as an associated action; executed after each other action?
    • Tick as a separate action? (Seems Better!!!)
      • Clock[p][d]
      • pvc[p][d]
    • Change <= in the waiting condition of UPDATE_REQUEST to <?
    • Using JavaTime?
      • NO! This would introduce a global wall clock.
  • Value
    • does not matter
    • can be eliminated
    • Now: Value = {v}
  • Client-server interaction
    • using msgs
    • well-formedness of clients
  • "wait until"
  • PMC
    • not necessary for TLA+

Progress

2020-01-15

  • Message
    • +REPLICATE
    • +HEARTBEAT
  • Clock
    • Tick as a separate action
      • Clock[p][d]
      • pvc[p][d]
    • Change <= in the waiting condition of UPDATE_REQUEST to <?
    • tick for Heartbeat
  • Computing CSS

2020-01-16

  • email
    • "latest version"
    • FIFO channel for propagating updates
    • UpdateCSS: css[m][d][d] not necessary?

2020-01-21

  • FIFO channel for propagating updates and heartbeats
    • incoming[p][d]
      • one incoming channel for each partition (NOW)
      • d \in Datacenter incoming channels for each partition
  • UpdateCSS:
    • Also computing css[m][d][d], for simplicity
  • i # d in Line 3 and Line 8
    • Delete such conditions, for simplicity

2020-01-23

  • Fixing one (pvc) ' problem
  • Fixing pvc updating error

2020-01-25

  • Delete Clock == Nat
  • Spec for CM: CausalMemory
    • +L[c] for history
      • Recording L[c] in ReadRequest & UpdateRequest
      • +OpTuple
    • causality order
      • so order
      • write-into order
  • Module Relation
    • +SeqToRel

2020-01-26

  • Handling NotVal in CM
    • Redefine Valid(s) with initial values for keys
  • Testing CM
    • +state constraint: \A c \in Client: Len(L[c]) <= 3

2020-01-27

  • Testing CM
    • FIXME: Range(seq) duplicate elements in sequence
      • +c : Client, cnt : Nat in OpTuple
  • CureKV:

2020-01-28

  • S[c] for serialization

2020-01-29

  • n^5 checking algorithm for CM

2020-01-30

  • CureKV

TODO

  • Version without Heartbeat
    • Check liveness
  • Properties
    • Safety
      • TypeOK
      • cvc[c] non-decreasing
      • css[p][d] non-decreasing
      • CM
    • Liveness

TLA+

  • googlegroup: "checking safety upon termination only?"
  • CostModel:

CostModel lookup failed for expression <line 54, col 36 to line 54, col 67 of module Cure>. Reporting costs into <line 52, col 22 to line 54, col 67 of module Cure> instead (Safety and Liveness checking is unaffected. Please report a bug.)