Distributed Systems, Time, Ordering, and Consistency - Complete Notes

A language-neutral guide to reasoning about partial failure, uncertain time, causal order, consistency contracts, partitions, and the production choices that make distributed behavior understandable, testable, and safe.

00. The distributed-systems mental model

A distributed system is a group of independent processes that cooperate by exchanging messages, while no participant can instantly know the complete current state of every other participant.

Distribution removes shared fate and enables geographic reach, independent scaling, and fault isolation. It also removes assumptions that are easy on one machine. Memory is not instantly shared. Message delay has no safe universal upper bound. Clocks do not exactly agree. A timeout is evidence of waiting, not proof of failure. Two healthy nodes can each be unable to reach the other. A useful design therefore begins with a system model and an observable contract, not a product name.

01. State the system model before reasoning

An algorithm is correct only relative to assumptions about processes, networks, clocks, and faults.

Synchronous, asynchronous, and partially synchronous networks

Synchronous model

Known upper bounds exist for message delivery and processing. Missing a bound can prove a fault, but real wide-area systems rarely preserve a tight bound during every overload or failure.

Asynchronous model

There is no known finite upper bound on message or process delay. A slow response and a failed node are indistinguishable from the observer's current evidence.

Partially synchronous model

Useful bounds eventually hold, or hold during normal periods, but the system does not know exactly when. Many practical coordination algorithms use this model for progress while preserving safety when timing assumptions fail.

Do not call an internal network reliable merely because packet loss is rare. Queueing, garbage collection, CPU starvation, connection-pool exhaustion, DNS failure, firewall changes, routing convergence, and overloaded peers can all look like loss. The end-to-end request observes the whole path, not the intended topology.

Common failure models

An ambiguous outcome is especially important. A client sends a payment command, the server commits it, and the reply is lost. The client sees a timeout but the payment happened. Retrying without an idempotency key may pay twice. Declaring failure without reconciliation may tell the user a lie.

02. Safety, liveness, and impossibility intuition

Safety says that nothing forbidden happens. Liveness says that something desired eventually happens.

• Safety: two confirmed orders never receive the same unique reservation.
• Safety: an acknowledged write is not silently replaced by an older version.
• Liveness: a valid request eventually receives a result when enough components recover.
• Liveness: replicas eventually converge after writes and partitions stop.

Safety is normally required in every execution admitted by the model. Liveness needs environmental conditions such as eventual message delivery, available quorum, bounded load, or a fair scheduler. Retrying forever can preserve the possibility of progress while violating a user's deadline. Returning immediately can improve response availability while violating a correctness invariant.

Reason with states and transitions

AVAILABLE
  -- reserve(request_id, deadline) --> HELD

HELD
  -- confirm(same request_id) ------> SOLD
  -- release(same request_id) ------> AVAILABLE
  -- expiry confirmed by authority -> AVAILABLE

SOLD
  -- ordinary retry ---------------> SOLD

Attach invariants to transitions. Only one authority may move an item from AVAILABLE to HELD for a given epoch. Replaying the same request ID returns the recorded transition. A stale holder from an older epoch cannot confirm after ownership changes. This exposes coordination requirements more clearly than saying the storage should be strongly consistent.

03. Physical time: wall clocks, monotonic clocks, skew, and drift

A clock reading is a measurement with error, not a universal ordering oracle.

Wall clock

Represents civil or UTC-related time for timestamps, schedules, certificates, and audit records. Synchronization may move it forward or backward, and leap-second handling differs by platform.

Monotonic clock

Advances in one direction for measuring elapsed time within one process or machine. Its origin is arbitrary, so readings from different machines are not directly comparable.

Skew

The difference between two clocks' readings at the same real instant.

Drift

The rate at which a clock gains or loses time relative to a reference.

Resolution

The smallest observable tick, which is not the same as accuracy.

Uncertainty

A bound or estimate around a reading within which the real time is believed to lie.

Network Time Protocol estimates offset using timestamp exchanges and disciplines local clocks, but asymmetric delays and faulty sources limit certainty. Synchronization reduces error; it does not make timestamps identical. Monitor offset, source health, stratum, reachability, and sudden steps. Set operational thresholds according to the feature: log correlation tolerates more error than a short security-token lifetime or a lease protocol.

long started = System.nanoTime();
long timeout = Duration.ofMillis(250).toNanos();

Result result = operation();

if (System.nanoTime() - started >= timeout) {
    return Result.timedOut();
}
return result;

Java documents that nanoTime() is for elapsed time and has an arbitrary origin. Use a subtractive comparison to handle numeric wraparound. Inject java.time.Clock for business time so expiry and scheduling tests are deterministic, but do not mistake a testable abstraction for a distributed ordering guarantee.

04. Timeouts are local decisions, not failure proofs

A timeout means an observer stopped waiting after its own deadline.

Client                    Service                   Store
  | POST payment K           |                        |
  |------------------------->| write K                |
  |                          |----------------------->|
  |                          |          committed     |
  |                          |<-----------------------|
  |  X response delayed     |                        |
  | timeout                  |                        |
  |                          |                        |

Client knows: no response arrived before its deadline.
Client does not know: whether the payment committed.

A failure detector converts observations such as missed heartbeats into suspicion. Aggressive thresholds detect failures quickly but falsely suspect healthy slow nodes. Conservative thresholds reduce false positives but delay failover. Measure heartbeat delay distributions and include processing pauses, not only network round trips. Use epochs or fencing whenever a falsely suspected old owner could still mutate state.

05. Causality and the happens-before relation

Causality asks whether one event could have influenced another, not which wall-clock timestamp is smaller.

Lamport's happens-before relation, written here as a -> b, follows three rules:

1. If events a and b occur in one process and a is first, then a -> b.
2. If a sends a message and b receives that message, then a -> b.
3. If a -> b and b -> c, then a -> c.

If neither a -> b nor b -> a, the events are concurrent in this model. They need not occur at the same physical instant. It means no causal path in the observed computation orders them. A deterministic tie-breaker may place concurrent events in a total display order, but it must not invent a causal dependency.

Process A:  a1 edit order ----send-----> a2
                                  
Process B:  b1 independent note      receive a1 -> b2 approve order

a1 -> b2 because a message carries the influence.
a1 and b1 are concurrent unless another path connects them.

Preserve causality explicitly through request IDs, trace context, parent event IDs, message offsets, and version metadata. Timestamps are useful evidence, but a clock correction can make a child log line appear earlier than its parent. For incident reconstruction, retain both wall time and protocol order.

06. Lamport logical clocks

A Lamport clock assigns numbers so causal order implies numeric order.

state counter := 0

before every local event:
  counter := counter + 1

when sending message m:
  counter := counter + 1
  m.logical_time := counter

when receiving message m:
  counter := max(counter, m.logical_time) + 1

ordering key when a total order is required:
  (logical_time, stable_process_id)

If a -> b, then L(a) < L(b). The converse is false: a smaller Lamport number does not prove causality. Lamport clocks are compact and useful for ordering replicated log proposals, audit events, or deterministic conflict application. They cannot by themselves detect that two versions are concurrent.

07. Vector clocks and version vectors

A vector records each participant's known progress so causal ancestry and concurrency can be distinguished.

For a fixed set of participants, maintain one counter per participant. A participant increments its own entry before an event, messages carry the vector, and receivers take the component-wise maximum before incrementing locally. Compare vectors V and W:

• V < W when every component of V is at most W and at least one is smaller. V is an ancestor.
• V = W when every component matches.
• They are concurrent when one has a larger component in one position and a smaller component in another.

def compare(left: dict[str, int], right: dict[str, int]) -> str:
    actors = left.keys() | right.keys()
    left_le = all(left.get(a, 0) <= right.get(a, 0) for a in actors)
    right_le = all(right.get(a, 0) <= left.get(a, 0) for a in actors)

    if left_le and right_le:
        return "equal"
    if left_le:
        return "ancestor"
    if right_le:
        return "descendant"
    return "concurrent"

A version vector is commonly associated with versions of a replicated object rather than every individual process event. The vocabulary varies across systems, so inspect the exact API. Metadata grows with actors. Practical systems use replica IDs instead of client IDs, dotted version vectors, bounded histories, or server-issued causal tokens. Truncating metadata can lose the ability to distinguish ancestry from concurrency and must be treated as a correctness trade-off.

Detect first, resolve second

08. A consistency model is an observable contract

Consistency does not mean one universal property. Name the scope, operations, and ordering rule.

First identify the object and boundary: one key, one partition, one session, a transaction, or the whole database. Then identify the history being constrained: reads and writes, all operations on an abstract object, or committed transactions. Finally state whether the order must respect program order, causality, or non-overlapping real-time order.

The word strong is too vague in a design contract. Replace it with linearizable per-key reads, strict-serializable transactions, bounded-staleness reads within five seconds, or causal session reads. A precise weaker guarantee is safer than an undefined stronger-sounding claim.

09. Evaluate histories, not marketing labels

A history satisfies a model only if a legal explanation exists under that model's rules.

Linearizable register example

real time --->

Client A: write(x=1) [invoke------response]
Client B:                              read(x) [invoke--returns 0]

This is not linearizable because the write completed before the read began, so the write must appear first in any real-time-respecting order. It might satisfy eventual consistency if the replica has not converged yet. If the read overlapped the write, returning 0 or 1 could both be linearizable because the atomic point could be placed before or after the write's atomic point.

Sequential but not linearizable

Client A: write(x=1) [done]
Client B:                    read(x) -> 0

Possible sequential explanation: read 0, then write 1.
Problem: that explanation reverses the observed non-overlapping real-time order.

Sequential consistency may permit this explanation if it preserves each client's own program order. Linearizability does not. This difference matters after a user receives a successful write and tells another user to read it.

Serializable but stale in real time

Transactions T1 and T2 can be serializable in the order T2 then T1 even if T1 completed before T2 began, unless the database also promises strict serializability or external consistency. Serializable answers whether transactions can be placed in a legal serial order. Linearizability concerns operations on an object and respects real-time precedence. They are related but not interchangeable.

10. Session guarantees and causal tokens

Session guarantees provide user-friendly behavior without forcing every replica read to be globally current.

A client can carry the highest version or causal dependency it has observed. A replica serves the request only after reaching that version, forwards to a sufficiently current replica, or reports that the requested guarantee cannot meet the deadline. Sticky routing is a simpler technique, but it fails over poorly and does not preserve the guarantee if the chosen replica loses state.

type SessionContext = { minimumVersion: string | null };

async function readOrder(id: string, session: SessionContext) {
  const response = await fetch(`/orders/${id}`, {
    headers: session.minimumVersion
      ? { "If-Version-At-Least": session.minimumVersion }
      : {},
  });

  const observed = response.headers.get("Observed-Version");
  if (observed) session.minimumVersion = maxVersion(session.minimumVersion, observed);
  return response.json();
}

Treat version tokens as untrusted input. Authenticate or validate their format, cap their size, and stop a client from demanding an impossible future version that pins resources. Tokens can reveal update rates, topology, or tenant activity, so expose opaque signed values when that metadata is sensitive.

11. CAP without slogans

CAP describes a forced choice during a network partition under specific definitions, not a menu for choosing any two letters.

In the Gilbert and Lynch formulation, consistency is atomic or linearizable behavior, availability means every request to a non-failing node eventually receives a response, and partition tolerance means the system must continue despite lost messages between groups. During a partition, two sides cannot both accept every conflicting operation and still act like one linearizable object. A design must sometimes refuse, delay, or redirect operations, or allow histories that are not linearizable.

Initial x = 0

        partition
Node A  X-----------X  Node B
write x=1              read x=?

If A confirms the write and B must answer without communication:
- B returns 0: response is available, but the object is not linearizable.
- B waits/refuses: linearizable behavior may be preserved, but this request is unavailable.
- B guesses 1: another possible write value makes guessing unsafe.

Partition tolerance is not normally optional because a real network can partition. The useful design question is per operation and per failure: which side retains authority, which reads may be stale, which writes can be merged, what error is returned, and how recovery reconciles state. A system can choose differently for catalog reads, inventory decrements, and analytics events.

12. PACELC and the normal-operation trade-off

Partitions are not the only time replicas trade latency for coordination.

PACELC asks: if there is a Partition, how does the system trade Availability against Consistency; Else, during normal operation, how does it trade Latency against Consistency? A synchronous cross-region write can provide a stronger visibility guarantee but must wait for distant communication. A local asynchronous write is faster but another region can lag or lose the newest acknowledged update during failover.

13. Database isolation is not distributed consistency

Isolation constrains concurrent transactions; distributed consistency constrains observations across copies and clients.

A database may provide serializable transactions on its primary while an asynchronous read replica returns an older committed state. Both claims can be true. A transaction can be serializable yet a message published outside it can be lost in a dual write. A linearizable single-row compare-and-set does not make a multi-row workflow serializable. Define each boundary independently.

PostgreSQL documents Serializable as behavior equivalent to some serial execution and warns that applications must retry serialization failures. That protects database invariants represented in the transaction. It does not automatically include an HTTP call, a file write, or another service.

14. Case study: a multi-region order status service

Choose different guarantees for commands, customer reads, support tools, and analytics instead of forcing one model everywhere.

Assumptions and requirements

• 8,000 order reads per second at peak and 800 state transitions per second.
• Three regions; customers read locally, while one authority owns each order at a time.
• Payment-confirmed must never move backward to payment-pending.
• A customer must see their successful update on the next page load.
• Other regions may show status up to five seconds old during normal operation.
• Analytics may be delayed and duplicated but must converge after replay.

First-pass design

Customer command
  -> regional API
  -> order authority for partition
  -> conditional state transition + durable version
  -> response {orderVersion, status}
  -> ordered change stream
  -> regional read projections
  -> analytics consumers

Next customer read carries minimum orderVersion.
Local projection serves it if caught up, otherwise forwards to authority or waits within budget.

Commands use a per-order monotonic version and a state-machine precondition. The authority rejects illegal transitions and makes a repeated command ID idempotent. The response returns the committed version. Regional projections provide fast reads; a causal token gives the writer read-your-writes. Other readers accept bounded staleness. Analytics consumes at-least-once changes with an idempotent event ID. This design spends coordination on irreversible transitions while keeping most reads local.

Behavior during a regional partition

Capacity and latency reasoning

With 8,000 reads per second and 90 percent served locally in 8 ms, about 800 reads per second reach an authority or lag-recovery path. If a partition removes local freshness, authority load can rise tenfold, so failover capacity must be sized for degraded mode or protected with admission control. At 800 transitions per second and 1 KB per change envelope, the raw change stream is about 800 KB/s before replication and protocol overhead. Retention, indexes, replicas, and replay headroom dominate the storage estimate more than the payload alone.

15. Production operations and observability

Observe uncertainty and contract violations, not only CPU and error counts.

Include node ID, process epoch, monotonic duration, wall timestamp, trace ID, request ID, object version, source replica, and consistency mode in structured telemetry where safe. Redact payloads and tenant-sensitive causal metadata. Dashboards should separate steady state from partition and failover behavior. An alert should name the violated user promise, not merely report replica lag.

16. Security, privacy, and trust boundaries

• Authenticate peers and authorize operations at the state owner. Transport encryption prevents observation and tampering in transit, but does not make a compromised peer correct.
• Treat replay as normal network behavior and as an attack technique. Bind idempotency keys to tenant, operation, payload digest, and expiry; reject reuse with different parameters.
• Sign or keep opaque client-carried version tokens. Validate length and provenance to prevent forged dependencies, resource pinning, metadata leakage, and cross-tenant access.
• Use fencing or epochs when ownership changes. Authentication of an old owner does not prove it is still authorized to mutate state.
• Protect time synchronization. Clock manipulation can affect certificate checks, token expiry, audit order, rate windows, and leases. Prefer several independent trusted sources and alert on steps.
• Causal graphs and precise timestamps may expose business relationships and user behavior. Apply data minimization, retention limits, access control, and deletion rules to operational metadata.

17. Performance, scalability, and cost trade-offs

Estimate coordination, not only request count. Measure round trips per operation, geographic RTT, serialized bytes, causal-context size, conflict-repair work, replica fan-out, and the load shift during failover. Tail latency often follows the slowest required dependency. Quorum and consistency choices therefore belong in capacity tables and cost reviews.

18. Failure scenarios and safer corrections

19. Testing consistency and recovery

Example-based unit tests validate algorithms; generated histories and faults validate distributed claims.

• Unit tests: verify logical-clock merge, vector comparison, state-machine transitions, token validation, idempotency, and deterministic conflict resolution.
• Model-based tests: generate operation sequences and compare the implementation against a small reference state machine.
• History checking: record invocation and response intervals, then search for a legal linearizable, sequential, causal, or serial explanation as appropriate.
• Integration tests: exercise real databases, brokers, replica reads, failover, causal token forwarding, and restart recovery.
• Fault tests: delay, drop, duplicate, and reorder messages; pause processes; skew clocks; fill queues; exhaust pools; partition one direction; and restart with old local state.
• Load tests: measure conflict rate, causal waiting, quorum latency, lag, and convergence under steady, burst, hot-key, and degraded-capacity workloads.
• Recovery tests: verify replicas converge, tombstones do not resurrect deleted data, epochs reject stale owners, and reconciliation explains every ambiguous command.

start three replicas and a history recorder
generate concurrent reads and conditional writes
after random intervals:
  partition replica A from B and C
  delay only A -> B messages
  pause one process
  move one wall clock backward
heal all faults
wait for the documented convergence bound

assert state-machine invariants
check completed history against promised model
assert all acknowledged writes are present or explicitly superseded
assert every client session preserved its requested guarantee

20. Production design checklist

• Write the process, network, clock, storage, and failure assumptions.
• Name the consistency guarantee per operation and data scope.
• Define behavior for timeout, partition, lag, failover, and recovery.
• Classify every result as committed, rejected, or ambiguous.
• Use monotonic time for local durations and wall time for civil timestamps.
• Preserve causal evidence through versions, sequence numbers, IDs, or tokens.
• Make conflict resolution match business semantics and remain auditable.
• Map replicas to independent failure and trust domains.
• Size and load-test the degraded path, not only the warm steady state.
• Monitor contract violations, lag, offset, conflicts, and reconciliation outcomes.
• Protect metadata and synchronization paths as security boundaries.
• Run recovery and history-checking tests before claiming a guarantee.

21. Hands-on exercises and design scenarios

Exercise 1: classify histories

Generate ten two-client register histories with overlapping and non-overlapping reads and writes. For each, decide whether it is linearizable, sequentially consistent, only eventually consistent, or invalid even under the application's convergence rule.

Expected reasoning: draw operation intervals, enforce real-time order only for non-overlapping operations, preserve each client's program order, and try to construct a legal sequential register execution. Do not use completion timestamps as atomic points.

Exercise 2: implement logical metadata

Implement Lamport clocks and vector comparison in one approved language. Simulate three replicas, deliver messages in different orders, and display which updates are ancestors or concurrent.

Expected reasoning: Lamport values provide a deterministic order but cannot prove concurrency. Vectors detect concurrency but grow with participants. Explain which metadata your production workload can afford.

Exercise 3: multi-region inventory

Design inventory for 100,000 products, 15,000 reads per second, 1,000 reservations per second, and three regions. Product descriptions may be stale for a minute; the last sellable unit must not be promised twice. State behavior during a region partition.

Expected reasoning: separate catalog reads from inventory transitions. Cache and replicate catalog data asynchronously. Give each inventory partition one current authority or pre-allocate bounded regional stock. Use conditional versioned transitions, idempotent reservation IDs, expiries with fencing, and reconciliation. Refuse unsafe reservations when authority or quota cannot be proved.

Exercise 4: incident reconstruction

Inject a two-second clock step on one node while a trace crosses four services. Reconstruct the request using parent spans, message IDs, offsets, and local monotonic durations rather than sorting wall timestamps.

Expected reasoning: wall time remains useful for correlating with external events, but protocol edges establish causality. Document uncertainty when two events remain concurrent.

22. Interview questions and model answers

1. Why is a timeout not proof that a server failed?

The observer knows only that no acceptable response arrived before its local deadline. The request may be queued, the server may be paused, the reply may be lost, or the operation may already have committed. A safe design uses idempotency, durable request status, bounded retries, and reconciliation. Follow-up: ask how the candidate prevents a stale recovered server from acting as owner.

2. What is the difference between wall and monotonic clocks?

Wall clocks represent civil time and may be corrected. Monotonic clocks measure elapsed duration within one clock domain and do not provide comparable global timestamps. Use monotonic time for timeouts and wall time for audit or schedules. Follow-up: ask why NTP does not make wall-clock last-write-wins safe.

3. What does happens-before mean?

It is a partial causal order formed by local program order, message send-before-receive, and transitivity. If neither event happens before the other, the events are concurrent in the model. Follow-up: ask whether a lower Lamport timestamp proves causality. It does not.

4. Compare Lamport and vector clocks.

Lamport clocks are compact and guarantee that causality implies increasing values, but the values cannot distinguish concurrency. Vector clocks use per-participant progress to identify ancestry, equality, and concurrency, at a metadata and membership cost. Follow-up: ask how actor churn and truncation affect correctness.

5. Explain eventual consistency precisely.

If updates stop and communication and processing continue, replicas eventually converge according to a defined resolution rule. It does not promise a fixed delay, fresh reads, preserved user intent, or absence of conflicts. Follow-up: ask how to turn eventual convergence into a five-second user-facing freshness SLO.

6. Sequential consistency versus linearizability?

Both seek a legal total order. Sequential consistency preserves each process's program order but may reorder non-overlapping operations from different processes. Linearizability also respects real-time precedence and places each operation's effect between invocation and response. Follow-up: ask for a history that is sequential but not linearizable.

7. What are session guarantees?

They constrain one client's observations, including read-your-writes, monotonic reads, monotonic writes, and writes-follow-reads. A causal or version token can preserve them across replicas without making every read globally current. Follow-up: ask what happens during failover when the target replica has not reached the token.

8. Explain CAP without saying choose two.

When communication is partitioned, isolated sides cannot both answer every conflicting request and preserve one linearizable object. The design chooses per operation whether to refuse or delay, route to an authority, serve stale data, or accept mergeable updates. Partition tolerance is a condition imposed by the network. Follow-up: distinguish CAP availability from an uptime SLO.

9. What does PACELC add?

It highlights that even without a partition, replica coordination trades latency against stronger consistency. During a partition the trade-off is availability versus consistency; else it is often latency versus consistency. Follow-up: compare a local asynchronous write with a cross-region quorum write.

10. Why is serializable isolation not the same as linearizability?

Serializability constrains whole transactions to be equivalent to some serial order. It need not preserve non-overlapping real-time order. Linearizability constrains operations on an object and does preserve real time. Strict serializability combines serial transaction behavior with real-time order. Follow-up: ask whether a serializable primary makes an asynchronous replica fresh.

11. How would you choose a consistency model for an order system?

Start from invariants and user harm. Coordinate payment and inventory transitions that cannot be safely merged. Provide read-your-writes after commands. Permit bounded-stale catalog and general status reads when acceptable. Let analytics converge through idempotent replay. State the scope and partition behavior for each operation. Follow-up: ask how degraded capacity changes the design during regional failure.

12. How do you test a consistency claim?

Record invocation and response intervals plus versions, generate concurrent workloads, inject realistic network, process, storage, and clock faults, and check histories against a formal model. Also verify convergence, acknowledged-write durability, session guarantees, and business invariants after recovery. Follow-up: ask why a happy-path integration test is insufficient.

23. Revision cheat sheet

• A distributed participant never has instant complete knowledge of the whole system.
• A timeout proves the deadline passed, not that the operation failed.
• Safety forbids bad states; liveness requires eventual progress under stated conditions.
• Partial failure means one component can fail while others continue.
• Use monotonic time for duration and wall time for civil timestamps.
• Clock synchronization bounds error; it does not create a perfect global order.
• Happens-before is a causal partial order based on processes and messages.
• Lamport clocks preserve causal direction but do not detect concurrency.
• Vector clocks detect ancestry and concurrency but add metadata and membership cost.
• Eventual consistency promises convergence after updates stop, not bounded freshness.
• Session guarantees improve one client's experience without forcing global freshness.
• Sequential consistency preserves program order; linearizability also preserves real time.
• Serializable transactions need not be strict serializable or make replicas current.
• CAP forces an availability-versus-linearizability choice during a partition.
• PACELC also exposes latency-versus-consistency choices during normal operation.
• Choose guarantees per operation from invariants, harm, latency, and failure behavior.
• Test histories, recovery, convergence, ambiguity, and degraded capacity.

24. Primary official references

• Leslie Lamport: Time, Clocks, and the Ordering of Events in a Distributed System - the happens-before relation and Lamport logical clocks.
• Gilbert and Lynch: Brewer's Conjecture and the Feasibility of Consistent, Available, Partition-Tolerant Web Services - the formal CAP result and its system-model definitions.
• Daniel Abadi: Consistency Tradeoffs in Modern Distributed Database System Design - the PACELC formulation and normal-operation latency trade-off.
• Herlihy and Wing: Linearizability, a Correctness Condition for Concurrent Objects - the original linearizability definition and history-based reasoning.
• Terry, Demers, Petersen, Spreitzer, and Theimer: Session Guarantees for Weakly Consistent Replicated Data - read-your-writes, monotonic reads, monotonic writes, and writes-follow-reads.
• Amazon Science: Dynamo, Amazon's Highly Available Key-Value Store - versioning, vector clocks, conflict reconciliation, and availability trade-offs.
• IETF RFC 5905: Network Time Protocol Version 4 - clock offset, delay, synchronization hierarchy, and discipline algorithms.
• Oracle Java System API documentation - wall-clock and monotonic elapsed-time semantics in Java.
• Google Cloud Spanner: TrueTime and external consistency - clock uncertainty, proper timestamping, external consistency, and MVCC reads.
• PostgreSQL: Transaction Isolation - serializable transaction behavior, anomalies, and retry requirements.