Brewer's Conjecture and the Feasibility of Consistent, Available, Partition-Tolerant Web Services
ACM SIGACT News, 2002 · paper · Computer science
Formalizes Brewer's conjecture that a web service cannot guarantee consistency, availability and partition tolerance together. Proves it in the asynchronous network model, then discusses ways around the dilemma in the partially synchronous model.
Checked: PDF from comp.nus.edu.sg, fetched 4 Oct 2026. Page numbers are those of that PDF.
4 findings
Substance "Theorem 4 The modified centralized algorithm is Delayed-t consistent." — the proof never addresses condition 3 of Definition 3 ("The order in P is consistent with the order of read and write requests submitted at each node"), and the printed algorithm admits an execution that violates it.
- p. 11 Theorem 4
The modified centralized algorithm is Delayed-t consistent.
- p. 9 Definition 3, condition 3
The order in P is consistent with the order of read and write requests
- p. 9 Definition 3, condition 2
by the previous write operation in P (or the initial value, if there is
- p. 10 Algorithm, write at A, step 3
sends an acknowledgement to the client.
Only the authors can say what is right here.
Judge's note: Read pages 9, 10 and 11 images and reworked the case. Let A be partitioned from C. A client writes v1 (not the initial value v0) at A; the message is lost, A times out and acknowledges the client (write step 3). A read is then submitted at A; its request is lost, and read step 3 returns the highest-sequence-number value received from C, or the initial value. A has received nothing from C carrying v1, so the read returns v0 (or an older value). By condition 2, write(v1) cannot be the previous write before this read in P; by condition 1 the read is ordered against every write; so the read precedes write(v1) in P. At node A the write was submitted before the read, which contradicts condition 3. Condition 3 has no "if messages are delivered" qualifier. The proof on page 11 argues the write ordering, atomicity when all messages are delivered, and the interval condition, but not condition 3. The proof's "earlier write operation at B_r" case suggests reads were meant to return locally written values, which would repair this; only the authors can say.
Second check: another model agreed
Report a problem with this finding
Reference or label Section 3.2.3 says "In Section 4.3 we consider some of the weaker consistency conditions that are possible", but weaker consistency conditions are in Section 4.4 "Weaker Consistency Conditions"; Section 4.3 is "Solutions in the Partially Synchronous Model".
- p. 7 Section 3.2.3, last sentence
In Section 4.3 we consider some of the weaker consistency condi-
- p. 8 Section 4.4 heading
Weaker Consistency Conditions
- p. 8 Section 4.4 heading
4.4 Weaker Consistency Conditions
- p. 7
In Section 4.3 we consider some of the weaker consistency conditions
Judge's note: Read page 7 image (the pointer) and page 8 image (headings 4.3 and 4.4). Section 4.3 describes the time-out variant of the centralized protocol and defines no consistency condition; Delayed-t consistency is introduced in 4.4. The pointer should read Section 4.4.
Second check: another model agreed
Report a problem with this finding
Reference or label Reference [6]: "Nancy Lynch. Distributed Algorithms, pages 397–350. Morgan Kaufman, 1996." — the page range runs backwards.
- p. 12 References, entry [6]
pages 397–350
- p. 12 Reference [6]
Distributed Algorithms, pages 397–350
- p. 12
Distributed Algorithms, pages 397–350.
Only the authors can say what is right here.
Judge's note: Read page 12 image: printed "pages 397–350". The end page is lower than the start page, so the range is impossible as printed. The correct range cannot be determined from the files, so this goes to the authors.
Second check: another model agreed
Report a problem with this finding
Wording Proof of Theorem 2: "The long interval of time in α2 ensures that the write request completes before the read request begins" — the long interval was built into α′2, not α2.
- p. 8 Proof of Theorem 2, second paragraph
The long interval of time in α2 ensures that the write request completes
- p. 8 Proof of Theorem 2, second paragraph
be an execution that begins with a long
- p. 8 Proof of Theorem 2
The long interval of time in α2 ensures
Only the authors can say what is right here.
Judge's note: Read page 8 image: this sentence prints plain α2, while the neighbouring occurrences carry the prime, so it is not an extraction artefact. Reworked: α′2 is defined as a long idle interval (at least as long as α1) followed by the events of α2; α2 from Theorem 1 is only a read request and response and has no idle interval. The step needs α′2. Reading α′2 for α2 repairs it and Theorem 2 stands.
Second check: another model agreed
Report a problem with this finding
5 minor (typos and the like; most checked by the judge only)
Wording The algorithm uses an undefined symbol t_timeout: "repeats step 4 within t − 4 ∗ t_timeout seconds" and "within time t − 2 ∗ t_timeout seconds"; the only time-out quantity defined is "2 ∗ t_msg + t_local" in Section 4.3.
- p. 10 write at A, step 5; New value received at C, step 3
peats step 4 within t − 4 ∗ttimeout seconds
- p. 8 Section 4.3
received within 2 ∗tmsg + tlocal, then the node concludes that the message
- p. 10 Algorithm, write at A step 5 and C step 3
peats step 4 within t − 4 ∗ ttimeout seconds.
- p. 10 New value at C, step 3
within time t −2 ∗ttimeout seconds.
Only the authors can say what is right here.
Judge's note: Read page 10 and page 8 images and searched the text: t_timeout appears only in the two algorithm steps on page 10 and is never defined or equated with 2*t_msg + t_local. That part is confirmed as an undefined symbol. The different multiples (4 for A's retry, 2 for C's resend) are unexplained but may be intended, since A's value must travel an extra hop; that part is not shown to be an error.
Second check: another model agreed
Report a problem with this finding
Wording Proof of Theorem 4 says "B_r must have received its value from the central node, C, or from an earlier write operation at B_r", but the printed read procedure returns only a value received from C or the initial value.
- p. 11 Proof of Theorem 4, last paragraph
its value from the central node, C, or from an earlier write operation at
- p. 10 read at node A, step 3
then return the value with the highest sequence number received
- p. 11 Proof of Theorem 4, third paragraph
or from an earlier write operation at
- p. 10 Algorithm, write at A, step 1
A sends a message to C with the new value.
Only the authors can say what is right here.
Judge's note: Read page 10 and page 11 images. Read step 2 returns C's response; step 3 returns "the value with the highest sequence number received from C ... or the initial-value". The write steps never store the new value locally for reads, and only C assigns sequence numbers. So the proof's "latter case" cannot arise under the pseudocode as printed, and the initial-value case is not treated. The former case covers the reads the printed algorithm can produce, so the argument for condition 5 is not broken; the proof and the pseudocode simply do not match.
Second check: another model agreed
Report a problem with this finding
Typo Misspelling in the proof of Theorem 2: "construct an admissable execution" (should be "admissible").
- p. 8 Proof of Theorem 2, first line on page
construct an admissable execution
- p. 8 Proof of Theorem 2, first line of page
and construct an admissable execution
Judge's note: Read page 8 image, first line: printed "admissable".
Second check: none (judge only)
Report a problem with this finding
Typo Inconsistent spelling: "acknowledgment" (Sections 3.2.1, 4.2, 4.3) versus "acknowledgement" (algorithm on page 10).
- p. 8 Section 4.3
or an acknowledgment
- p. 10 write at A, step 2
If A receives an acknowledgement from C
Judge's note: Page 8 image prints "acknowledgment" three times; page 10 image prints "acknowledgement" throughout the algorithm. A text search confirms the split. Both spellings are valid; only the inconsistency is at issue.
Second check: none (judge only)
Report a problem with this finding
Typo References [6]–[9] print the publisher as "Morgan Kaufman".
- p. 12 References [6]–[9]
Morgan Kaufman
Only the authors can say what is right here.
Judge's note: Rests on outside knowledge: that the publisher's name is spelled "Morgan Kaufmann" with a double n. The page 12 image prints "Morgan Kaufman" in all four Lynch entries, so it is not an extraction artefact; the correct spelling cannot be verified from the files.
Second check: none (judge only)