Atomic replication

                        v
                        ┌─────►@саша
                        │      │
            ┌ ─ ─ ─ ─ ──│─┐    │ Get(k)
            │ ┌─┐       │ │    │
            │ └─┘    ┌─┐◄──────┘
            │        └─┘  │
            │   ┌─┐       │
         ┌──────└─┘       │
     Ack |  |    ▲        |
         │  └ ─ ─│─ ── ─ ─┘
         │       │
         ▼       │ Set(k, v)
         @вася───┘
  • обобщение понятия модели памяти
[Impl]

History h:
 w(1): [------]
   w(2): [-------]
          R: [----------]
--------------------------------->
                              time
[Spec]

 w(2) w(1) R w(3) R
       ▲   │  ▲   │
       └───┘  └───┘
  • Хотим Linearizability ~ External consistency (consistency models)
    • Для любой истории h из Impl существует линеаризованная история h* такая, что для любых двух событий O1 и O2 из h таких, что O1 завершилось до начала O2: в h* O1 следует перед O2.
  • Пользователю не важно точное время, но важно отношение причинности happens-before
  • Если события упорядочены во времени, то они упорядочены и по happens-before

Solutions