Towards Bug-Free Distributed Go Programs

Zhengqun Koo

REVIEW 4 major objections 4 minor 47 references

Towards Bug-Free Distributed Go Programs

T0 review · 4 major / 4 minor · reviewed 2026-08-15 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read A verification framework for a subset of Go can prove that an implementation satisfies a global communication protocol, and if the protocol is race-free, the implementation is guaranteed to have no communication races.

desk verdict The paper's central race-freedom guarantee is unsupported: Conjecture 1 is false and the guard-proving rule leans on a lemma the appendix itself proves unsound. read the letter →

arxiv 2506.15135 v2 pith:G6WIKLJW submitted 2025-06-16 cs.SE cs.LOcs.PL

Zhengqun Koo This is my paper · ORCID

classification cs.SEcs.LOcs.PL

keywords communicationracesGoconcurrencyhappens-beforeorderglobalprotocolssessionlogicdeductiveverificationFIFOchannelsrendezvous

verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

This paper describes a static verification framework for a subset of the Go language that uses message passing for synchronization, and its goal is to certify that a distributed Go program is free of communication races. A communication race occurs when concurrent sends and receives on a shared FIFO channel are not ordered by a happens-before relation, so a receiver can end up reading a message intended for another receiver or reading nothing at all. The framework takes a specification in the form of a global protocol, inserts guards that require certain happens-before facts to be proved, and then verifies the implementation by projecting the protocol onto goroutines and channel endpoints and checking each endpoint with a program-logic triple. The paper's central claim is that if verification of an implementation against a race-free global protocol succeeds, then users can be certain the implementation is race-free in every interleaving.

What carries the argument

The load-bearing objects are the guarded race-free global protocol and the happens-before order over event starts and completions. A global protocol is a session-logic expression built from transmissions of the form P^i -c*-> P'^i, guards ¸(E zHB E'), the empty protocol, sequential composition, and concurrent composition; each guard is a proof obligation that the implementation must discharge. The machinery that carries the proof is the two-stage projection (global to per-party, then per-party to per-endpoint), which produces independent per-endpoint protocols verified by data-send, data-receive, endpoint-send, and endpoint-receive rules, plus a guard-proving rule. To discharge a guard, the projected protocol inserts a rendezvous on a fresh unbuffered channel and applies the semantic condition (bef-sends are before-recvs), which the paper derives from a propagation lemma that it later proves unsound for buffered channels.

What would settle it

Write a small Go program with two concurrent sends and two concurrent receives on a shared unbuffered channel, where a rendezvous fixes the send order but the receive order is reversed (so the second receive can take the first message), run the verifier, and see whether any guard is discharged; if the verifier certifies the program race-free, or a trace shows the condition (bef-sends are before-recvs) implying E zHB ER while a concurrent receiver exists, the central guarantee fails.

Watch

Extended reading notes

Core claim

The central discovery is that communication-race freedom for Go can be reduced to a shape property of global protocols plus a set of guard proof obligations. The paper distinguishes a communicates-before order, which records which send is supposed to match which receive, from a happens-before order that includes both the starts and completions of send and receive events; this distinction lets a rendezvous on an unbuffered channel be represented without violating the asymmetry of happens-before. Race-freedom is then ensured by inserting guards into the protocol that require the sends on a shared channel to be linearly ordered by happens-before, and the receives to be linearly ordered in the same way, so that the FIFO property cannot deliver a message to the wrong receiver. Verification works by projecting the guarded protocol first onto each party and then onto each channel endpoint, and consuming the resulting per-endpoint protocols with program-logic triples; a successful global verification is the certificate that the implementation is race-free.

Load-bearing premise

The guarantee rests on the semantic condition (bef-sends are before-recvs) used when proving guards: the paper derives this condition from a propagation lemma it later proves unsound for buffered channels, and never proves the unbuffered instance sound, so a racy implementation could in principle be certified if that inference fails.

Editorial extensions

If this is right

A Go program that passes verification against a race-free global protocol is guaranteed never to deliver a message to the wrong receiver or leave a receiver empty, in any interleaving.
Any global protocol with races can be mechanically transformed into a race-free protocol by inserting guards that linearly order the sends and the receives on each shared channel.
Verification is modular: each goroutine's and each channel endpoint's protocol can be checked independently, so the workload can be parallelized and failures pinpoint the exact party, endpoint, and line.
The framework reasons statically about all possible sequential executions of the program, so it detects races that a single dynamic run would miss.
The framework simplifies the prior session-logic verification by dropping the dual of guards, while restricting synchronization to rendezvous on unbuffered channels.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

If the unbuffered instance of the (bef-sends are before-recvs) condition is genuinely unsound, the failure would appear not as a verifier crash but as a false certificate: a program with a communication race that passes. A stress test that feeds the verifier systematically generated racy rendezvous patterns would settle whether this gap is real.
The per-endpoint projection suggests a natural incremental-verification strategy: after a code change, only the endpoints whose send or receive lines changed need to be re-verified, so long as the global protocol is unchanged.
The same guard-and-projection schema could be applied to other communication orderings, such as causal or total message order, by substituting the appropriate ordering rules for the FIFO rules; the paper notes this direction but does not implement it.
A practical companion tool built on this framework would need to handle Go's full synchronization zoo beyond unbuffered channels, including buffered channels with positive capacity, mutexes, and WaitGroups, so extending the framework is an open engineering problem.

Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Desk Editor's Note

read the letter

Quick take: the main claim — that successful verification against a race-free global protocol certifies race-freedom — is not just unproven; it is false as stated. Conjecture 1, which bridges guards to race-freedom, fails on a simple counterexample, and Section 10.1's guard-proving step uses a semantic condition derived from a lemma the paper itself proves unsound in Appendix 14.1. That is a load-bearing problem, not a cosmetic one.

What is genuinely there: the partial-order representation of global protocols, guards as zHB proof obligations, and the start/completion event model for rendezvous are real extensions of Costea's session logic. The motivation is good — shared FIFO channels in Go can deliver messages to the wrong receivers — and the paper is honest about several gaps: projection fidelity is cited and omitted, and the appendix explicitly proves (HB-CB) unsound. That honesty works in the author's favor; it makes the internal contradiction easy to see.

The soft spots, in proportion: Conjecture 1 is false. Take G = (A1 ->c2 B) * (C2 ->c2 D) on one channel of capacity 2. The linear order A1, C2, D2, B1 is legal: both sends buffer, the first receive (D2) takes A1's message, and the second receive (B1) takes C2's. This order extends zHB∪zCB, since A1 precedes B1 and C2 precedes D2. But D2 gets the wrong sender, and so does B1 — exactly the race the paper defines. The conjecture's only-if direction fails, and Sections 9.2 and 9.3 lean on it. Separately, the guard proof in Section 10.1 relies on (bef-sends are before-recvs), which the appendix derives from (HB-CB) and then proves unsound; the c0 instance is never shown sound. Without that, guards can be discharged incorrectly. The paper also ships no tool and no machine-checked proofs, so there is no external check on these steps.

Who this is for: a reader looking for ideas about partial-order session logic for Go might skim it, but nobody should rely on its correctness guarantees. It reads like a dissertation draft — which it is — and it would need a corrected conjecture, a proof or clearly restricted claim, and a fix for the HB-CB self-contradiction before it could stand as a paper.

My recommendation: desk-reject as-is. The counterexample and the internal contradiction are fixable starting points, and the author should be told about them directly.

Referee Report

4 major / 4 minor

Summary. The paper presents a deductive verification framework for a subset of Go intended to prove the absence of communication races. It models global protocols as partial orders over send and receive events, introduces a happens-before order zHB and a communicates-before relation zCB, and extends Go's memory-model rules to buffered and unbuffered channels. Verification proceeds by projecting a global protocol to per-party and per-endpoint protocols, then checking implementations with Hoare-style rules; guards are proof obligations for zHB facts used to make protocols race-free. The central claim, stated in Section 11, is that if verification succeeds against a race-free global protocol, then users can be certain the implementation is race-free. This claim rests on Conjecture 1 (Section 8.3), which asserts that sequential executions whose linear order extends the union of zHB and zCB are exactly the race-free ones.

Significance. If the central guarantee were sound, the framework would be a genuinely useful deductive approach to communication race-freedom in Go, and the modular per-endpoint projection is an attractive design. The paper also deserves credit for explicitly modeling Go's channel rules (3a) and (3b), for distinguishing buffered from unbuffered channels, and for honestly proving in Appendix 14.1 that one of Costea's propagation lemmas, (HB-CB), is unsound. However, the main advertised result is not established: Conjecture 1 is unproven and in fact false as stated; the guard-discharge rule in Section 10.1 relies on a semantic condition whose soundness is not proved and whose source lemma is shown unsound; and projection fidelity is delegated to an omitted external proposition. Because these gaps are load-bearing for the Section 11 certainty claim, the manuscript in its current form does not support its central conclusion.

major comments (4)

[Section 8.3, used in Sections 9.2, 9.3, and 11] Conjecture 1 is false as stated. Consider the global protocol G = (A^1 ->_{c^2} B) * (C^2 ->_{c^2} D), where both transmissions share a FIFO channel c of capacity 2 and are concurrently composed, so there are no cross-party zHB edges. The zCB order is {A1 -> B1, C2 -> D2}. The linear order A1, C2, D2, B1 is a legal sequential execution: both sends may be buffered before either receive, and FIFO delivers A1's message to D2 and C2's message to B1. This order extends the union zHB ∪ zCB, since A1 precedes B1 and C2 precedes D2, yet by the paper's own race-freedom definition in Section 8.3 the execution is racy because neither receiver obtains its protocol-specified sender. Thus the 'if' direction of Conjecture 1 fails. Since Sections 9.2 and 9.3 explicitly rely on Conjecture 1 to conclude that proved guards imply race-freedom, and Section 11 states the certainty guarantee, the central claim is unsupported even before considering the guard-proving step.
[Section 10.1, Figure 9, and Appendix 14.1] The rule that discharges guards is not justified. In Section 10.1, step 2, the verification derives P'i zHB P''h by applying the semantic condition (bef-sends are before-recvs) from Figure 9. Appendix 14.1 states that this condition is derived from Costea's propagation lemma (HB-CB), and then Lemma 2 proves that (HB-CB) is unsound for buffered channels. No soundness proof is given for the c0 (unbuffered) instance of the condition, and Appendix 14.1.2 explicitly says the authors only suspect, without proof, that the related lemma (CB-HB) is sound. Because guard discharge is the only mechanism connecting successful verification to the race-freedom guarantee, this missing proof is load-bearing: without it, a racy implementation could in principle be certified.
[Section 10.1, Projection] Projection fidelity is essential for reducing verification of a global protocol to verification of independent per-party and per-endpoint protocols, but the paper says only that 'Projection fidelity was shown in [8, Proposition 1] and is omitted in this work.' Since the cited source is an unpublished thesis and the proposition is not reproduced or restated, the soundness argument is incomplete at a central point. The omitted proposition is not a presentation detail; it is the step that lets successful per-endpoint verification imply satisfaction of the global protocol, which is a prerequisite for the Section 11 guarantee.
[Section 9.2, transformation to race-free protocols] The transformation inserts guards only 'for each pair of transmissions ordered by the ; operator,' but its stated goal is to linearly order all sends and all receives on a shared channel so that the zCB(·) mapping is isotone. For global protocols that use concurrent composition over the same channel, such as (A^1 ->_{c^2} B) * (C^2 ->_{c^2} D), pairs of transmissions in different concurrent branches are not ordered by ';' and receive no guards. No additional rule is given for such cross-branch pairs, so the transformation as described cannot establish the required linear orders, and the race-free guarantee fails exactly for the class of protocols exhibited in the Conjecture 1 counterexample.

minor comments (4)

[Manuscript structure] The submission appears to concatenate a literature review report, the dissertation itself, and a slide deck, with duplicated material and broken cross-references (for example, 'section ??' appears in the slide portion and in Section 13.2). The manuscript should be consolidated into a single coherent paper with consistent numbering.
[Bibliography] Several bibliography entries are garbled or inconsistently formatted, e.g. '[38]Liu2021AutomaticallyDA8668036', '[6]DY2013lange2018veriﬁcationgabet2020static', and '[18]Hoare2009ConcurrentKA'; the reference numbering also differs between the earlier literature-review part and the main dissertation part.
[Section 10.1, projection of guards] The projection rule for a guard uses 'for some d0' without stating a freshness side condition. Since Requirement 1 in Section 8.2 demands that the unbuffered channel of a rendezvous be used only by that pair of events, the rule should explicitly require that distinct guards project to distinct fresh unbuffered channels.
[Figures and notation] The guard symbol is rendered inconsistently (for example, as '¸'), and some figure references inside the slide portion point to undefined sections; these should be typeset and cross-referenced uniformly.

Circularity Check

1 steps flagged · score 6.0 of 10

Central race-freedom guarantee restates the definition of 'race-free global protocol'; the substantive bridge (Conjecture 1) is unproven and one cited propagation lemma is shown unsound.

self definitional [Section 4.2 (definition) and Section 11 (conclusion), relied on in Sections 9.2 and 9.3]
""If a global protocol may be satisfied by an implementation which may execute with races, then we call this a 'global protocol with races'. Otherwise, we call this a 'race-free global protocol'." ... "If our verification determines that an implementation satisfies a race-free global protocol, then users of our verification framework can be certain that the implementation is race-free.""

The predicate 'implementation satisfies a race-free global protocol' is defined in Section 4.2 as: the protocol cannot be satisfied by any implementation that may execute with races. The Section 11 guarantee is therefore the definiens of 'race-free global protocol' instantiated on the implementation, not a theorem derived from the Hoare-triple verification machinery. The actual content — that the guard-insertion transformation, projections, and guard-proving rules produce a protocol falling in this semantic class — is carried by Conjecture 1 (Section 8.3), which is explicitly unproven, and Section 9.3 relies on it directly: 'all sequential executions subsumed by this concurrent execution are race-free by conjecture 1'.

full rationale

One genuinely circular step is present: the paper's headline guarantee (Section 11) is exactly the definition of 'race-free global protocol' given in Section 4.2, so the implication 'satisfies a race-free global protocol implies race-free implementation' is a tautology unpacking the defined term, not a derived soundness theorem. The rest of the derivation chain is better described as unsupported or incorrect rather than circular: (a) Section 8.3 states the key bridge as 'Conjecture 1' and Section 9.3 relies on it directly; (b) Section 10.1's guard proof applies the semantic condition (bef-sends are before-recvs), which Appendix 14.1 says is derived from Costea's (HB-CB) propagation lemma, but Lemma 2 then proves (HB-CB) unsound, and no soundness proof for the c0 instance is supplied; (c) projection fidelity, which licenses the reduction from global to per-endpoint verification, is cited to Costea [8, Proposition 1] and omitted in this work. These are correctness gaps rather than self-definitional reductions. No fitted parameters or empirical predictions are involved, so there is no fitted-input circularity. Because the central certainty-of-race-freedom statement is guaranteed by definition while the structural route to that definition is unproven, the score reflects partial circularity, not full equivalence.

Assumptions & free parameters 0 free parameters · 7 assumptions · 2 invented entities

The framework is not self-contained: it assumes Go's memory model, fixed parties, sequential consistency up to races, Costea's omitted projection-fidelity result, and its own unproven conjecture, while using a semantic condition derived from a lemma it proves unsound. No numeric parameters are fitted.

assumptions (7)

domain assumption All channels are FIFO and have types matching the events sent on them.
Stated in Section 1.2 (Literature Review) and Section 4.4: Go channels are FIFO and typed; the framework assumes this model.
domain assumption Go memory model rules (3a) and (3b) correctly describe the happens-before order induced by sends and receives.
Section 5, Figure 4: these rules are taken as the semantics of channel communication, including the role of buffer capacity k.
domain assumption Parties (goroutines performing send or receive) are fixed in advance; dynamic spawning of parties is disallowed.
Section 7: 'All concurrently executing parties must be determined in advance' and models that permit dynamic spawning are excluded.
domain assumption Go executions with only sends and receives are sequentially consistent up to communication races.
Section 5: 'We believe this claim of sequential consistency also holds for the memory model of Go, for executions up to when the execution has a communication race'; based on Fava et al. [13] for data-race-freedom but not proven here.
ad hoc to paper Semantic conditions in Figure 9 (especially 'bef-sends are before-recvs') are sound for unbuffered channels.
Section 8.2 states these conditions as requirements; Section 14.1 derives them from Costea's propagation lemmas and proves (HB-CB) unsound, but does not re-prove the c0 instances.
domain assumption Projection fidelity of global protocols to per-party and per-endpoint protocols (Costea [8, Proposition 1]).
Section 10.1: 'Projection fidelity was shown in [8, Proposition 1] and is omitted in this work'; the modular verification relies on this.
ad hoc to paper Conjecture 1 characterizes race-free sequential executions by linearizations of the union of zHB and zCB.
Section 8.3 states this as a conjecture without proof and uses it to justify race-freedom reasoning; no soundness proof is supplied.

invented entities (2)

Guard g(Psi)
purpose: Proof obligation inserted into a global protocol that must be discharged by verification before later protocol segments are checked; used to enforce event orderings such as A1 zHB B2.
Introduced in Section 9; a syntactic construct with no external falsifiable handle beyond the framework's own verification semantics.
zCB (communicates-before) relation
purpose: Distinguishes 'should receive from' (protocol expectation) from actual happens-before, defining communication races.
Introduced in Section 7.1; internal ordering relation, not an externally testable quantity.

how reviews work

0 comments

Cite this review

Pith. "Pith review of Towards Bug-Free Distributed Go Programs." pith.science (2026). https://pith.science/paper/G6WIKLJW

@misc{pith2026250615135,
  author       = {Pith},
  title        = {Pith review of: Towards Bug-Free Distributed Go Programs},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/G6WIKLJW}},
  note         = {Machine review of arXiv:2506.15135}
}

read the original abstract

Programmers of distributed systems need to reason about concurrency to avoid races. However, reasoning about concurrency is difficult, and unexpected races show up as bugs. Data race detection in shared memory systems is well-studied (dynamic data race detection [13], behavioral types [15], dynamic race detection [31]). Similar to how a data race consists of reads and writes not related by happens-before at a shared memory location, a communication race consists of receives and sends not related by happens-before on a shared channel. Communication races are problematic: a receiver expects a specific message from a specific sender, but with a communication race, the receiver can receive a message meant for another receiver, or not receive anything at all. In this work, we describe a verification framework that can prove the absence of communication races for distributed programs that use a subset of the Go programming language, where synchronization is mainly achieved via message passing. We statically reason about how a distributed program executes, using a happens-before order, extended to buffered and unbuffered channels.

Figures

Figures reproduced from arXiv: 2506.15135 by the authors.

**Figure 2.** Communication races no longer happen when no sends are concurre [PITH_FULL_IMAGE:figures/full_fig_p006_2.png] view at source ↗

**Figure 1.** A line of code <-c in party A is abstracted away to become an event AR. Execution of the line of code starts at the upper dotted line, and completes at the bottom dotted line. The duration of the event is defined by these two dotted lines. The goal of this work is to describe a verification framework that can verify that an implementation satisfies a specification. Users of our framework should follow the following … view at source ↗

Figures from the paper (21 more)

**Figure 2.** Figure 2: This figure shows two sets of programs, and two sets of protocols. [PITH_FULL_IMAGE:figures/full_fig_p024_2.png]

**Figure 3.** Figure 3: Terminology describing the start and completion of an event. [PITH_FULL_IMAGE:figures/full_fig_p028_3.png]

**Figure 4.** Figure 4: Rules governing sends and receives, from the memory model [PITH_FULL_IMAGE:figures/full_fig_p028_4.png]

**Figure 5.** Figure 5: These executions demonstrate the blocking behavior of the [PITH_FULL_IMAGE:figures/full_fig_p028_5.png]

**Figure 6.** Figure 6: Rendezvous executions between events A1 and B1 on channel c 0 , one where events happen instantaneously, and one where events happen over a duration. parts of an event. Similarly, the two B1 refer to distinct parts of an event. The execution 6b captures this notion. No…

**Figure 7.** Figure 7: Sequence diagrams of global protocol (4a), one without guards, and one wi [PITH_FULL_IMAGE:figures/full_fig_p037_7.png]

**Figure 8.** Figure 8: An illegal sequential execution of the global protocol 7a. [PITH_FULL_IMAGE:figures/full_fig_p039_8.png]

**Figure 9.** Figure 9: Semantic conditions for channel c 0 . (aft-recvs are aft-sends) and (bef-sends are before-recvs), because these are already satisfied by ordering the send before the receive.7 The sequential execution must satisfy condition (bef-recvs are before-sends) such that no eve…

**Figure 10.** Figure 10: Sequential executions of the rendezvous execution 6b, one wi [PITH_FULL_IMAGE:figures/full_fig_p041_10.png]

**Figure 11.** Figure 11: Sequential executions of global protocol 7a, one race-free, and one w [PITH_FULL_IMAGE:figures/full_fig_p042_11.png]

**Figure 12.** Figure 12: The guarded global protocol converted from the global protocol with r [PITH_FULL_IMAGE:figures/full_fig_p044_12.png]

**Figure 13.** Figure 13: A global protocol and its concurrent execution with the send-r [PITH_FULL_IMAGE:figures/full_fig_p046_13.png]

**Figure 14.** Figure 14: The guarded global protocol 12 but race-free, and its race-free se [PITH_FULL_IMAGE:figures/full_fig_p047_14.png]

**Figure 15.** Figure 15: The syntax of global protocols, per-party protocols, and per-end [PITH_FULL_IMAGE:figures/full_fig_p050_15.png]

**Figure 16.** Figure 16: Protocol structural congruence, where Protocol is either [PITH_FULL_IMAGE:figures/full_fig_p050_16.png]

**Figure 17.** Figure 17: The projection functions. 33 [PITH_FULL_IMAGE:figures/full_fig_p052_17.png]

**Figure 18.** Figure 18: Verification rules and lemmas. 38 [PITH_FULL_IMAGE:figures/full_fig_p057_18.png]

**Figure 19.** Figure 19: The unconsidered sequential execution in an example from Fav [PITH_FULL_IMAGE:figures/full_fig_p064_19.png]

**Figure 20.** Figure 20: Costea’s propogation lemmas. 14 Appendix 14.1 Soundness or unsoundness of (HB-CB) and (CB-HB) The semantic conditions (aft-recvs are aft-sends) and (bef-sends are before-recvs) are derived respectively from Costea’s (CB-HB) and (HB-CB) propogation lemmas [8], where co…

**Figure 21.** Figure 21: The one-transmission sequentially composed global protocol cons [PITH_FULL_IMAGE:figures/full_fig_p067_21.png]

**Figure 22.** Figure 22: The transitive closure of sequential execution 14b. [PITH_FULL_IMAGE:figures/full_fig_p068_22.png]

Review history (2 revisions) →

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

47 extracted references · 47 canonical work pages

[1]

Adve, S., Hill, M., Miller, B., and Netzer, R. (1991). Detect ing data races on weak memory systems. volume 19, pages 234–243

work page 1991
[2]

Bocchi, L., Demangeon, R., and Yoshida, N. (2012). A multi party multi-session logic. In TGC

work page 2012
[3]

Brookes, S. (2007). A semantics for concurrent separati on logic. Theoretical Computer Science , 375(1):227–270. Festschrift for John C. Reynolds’s 70th bir thday

work page 2007
[4]

and O’Hearn, P

Brookes, S. and O’Hearn, P. (2016). Concurrent separatio n logic. ACM SIGLOG News , 3:47–65

work page 2016
[5]

and Pfenning, F

Caires, L. and Pfenning, F. (2010). Session types as intui tionistic linear propositions. In CONCUR

work page 2010
[6]

Castro, D., Hu, R., Jongmans, S.-S., Ng, N., and Yoshida, N. (20 19). Distributed programming using role-parametric session types in go: Statically-typ ed endpoint apis for dynamically-instantiated communication structures. Proc. ACM Program. Lang. , 3(POPL)

work page
[7]

Automated Verification of CountDownLatch

Chin, W., Le, T. C., and Qin, S. (2019). Automated veriﬁcati on of countdownlatch. ArXiv, abs/1908.09758

work page Pith review arXiv 2019
[9]

Craciun, F., Kiss, T., and Costea, A. (2015). Towards a sess ion logic for communication protocols. In 2015 20th International Conference on Engineering of Complex Computer Systems (ICECCS) , pages 140–149. IEEE

work page 2015

Show all 47 references

[10]

and Yoshida, N

Deni´ elou, P.-M. and Yoshida, N. (2013). Multiparty Com patibility in Communicating Automata: Characterisation and Synthesis of Global Session Types. In 40th International Colloquium on Automata, Languages and Programming , volume 7966 of LNCS, pages 174–186. Springer

2013
[11]

and Sato, H

Ding, Y. and Sato, H. (2020). Formalizing and verifying de centralized systems with extended concurrent separation logic

2020
[12]

Fava, D. S. and Steﬀen, M. (2020). Ready, set, go! data-r ace detection and the go language

2020
[13]

S., Steﬀen, M., and Stolz, V

Fava, D. S., Steﬀen, M., and Stolz, V. (2018). Operationa l semantics of a weak memory model with channel synchronization. In Havelund, K., Peleska, J., R oscoe, B., and de Vink, E., editors, Formal Methods, pages 258–276, Cham. Springer International Publishing

2018
[14]

and Yoshida, N

Gabet, J. and Yoshida, N. (2020). Static race detection an d mutex safety and liveness for go programs (extended version). 49

2020
[16]

Gerrand, A. (2010). Share memory by communicating

2010
[17]

Gibson-Robinson, T., Armstrong, P., Boulgakov, A., and R oscoe, A. (2013). Failures Divergences Reﬁnement (FDR) Version 3

2013
[18]

Gischer, J. L. (1988). The equational theory of pomsets. Theor. Comput. Sci. , 61:199–224

1988
[20]

Hoare, C., M¨ oller, B., Struth, G., and Wehrman, I. (2009 ). Concurrent kleene algebra. In CONCUR

2009
[21]

Hoare, C. A. R. (1978). Communicating sequential processe s. Commun. ACM , 21(8):666–677

1978
[22]

Honda, K., Yoshida, N., and Carbone, M. (2008). Multipart y asynchronous session types. In Proceedings of the 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’08, page 273–284, New York, NY, USA. Association for Computi ng Machinery

2008
[23]

Jaskolka, J., Kh´ edri, R., and Zhang, Q. (2014). Endowing concurrent kleene algebra with communication actions. In RAMICS

2014
[24]

and Ross, K

Kurose, J. and Ross, K. (1999). Computer networking - a to p-down approach featuring the internet

1999
[25]

Labelle, G. (2000). Counting enriched multigraphs acc ording to the number of their edges (or arcs). Discrete Mathematics , 217(1):237–248

2000
[26]

Lamport, L. (1978). Time, clocks and the ordering of eve nts in a distributed system. Communications of the ACM 21, 7 (July 1978), 558-565. Reprinted in several collections, including Distributed Computing: Concepts and Implementations, McEntire et al., ed. IEEE Press, 1984. ,...

1978
[27]

Lange, J., Ng, N., Toninho, B., and Yoshida, N. (2017). Fenci ng oﬀ go: Liveness and safety for channel-based programming. SIGPLAN Not. , 52(1):748–761

2017
[28]

Liu, Z., Zhu, S., Qin, B., Chen, H., and Song, L. (2021). Aut omatically detecting and ﬁxing concurrency bugs in go software systems

2021
[29]

Mathur, U., Pavlogiannis, A., and Viswanathan, M. (2021). Optimal prediction of synchronization- preserving races. Proceedings of the ACM on Programming Languages , 5:1 – 29

2021
[30]

and Yoshida, N

Ng, N. and Yoshida, N. (2016). Static deadlock detection fo r concurrent go by global session graph synthesis. In Proceedings of the 25th International Conference on Compiler Construction , CC 2016, page 174–184, New York, NY, USA. Association for Computing Machine ry

2016
[31]

OEIS Foundation Inc. (2021). The on-line encyclopedia of integer sequences

2021
[32]

and Huisman, M

Oortwijn, W. and Huisman, M. (2019). Practical abstracti ons for automated veriﬁcation of message passing concurrency. In Ahrendt, W. and Tapia Tarifa, S. L., ed itors, Integrated Formal Methods , pages 399–417, Cham. Springer International Publishing

2019
[33]

and Pradubsuwun, D

Prasertsang, A. and Pradubsuwun, D. (2016). Formal veri ﬁcation of concurrency in go. In 2016 13th International Joint Conference on Computer Science and Software Engineering (JCSSE) , pages 1–4. 50

2016
[34]

Smaragdakis, Y., Evans, J., Sadowski, C., Yi, J., and Flanaga n, C. (2012). Sound predictive race detection in polynomial time. In Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages , POPL ’12, page 387–400, New York, NY, USA. As...

2012
[36]

package ssa

The Go Authors (2020a). package ssa

2020
[37]

package sync

The Go Authors (2020b). package sync

2020
[38]

Tu, T., Liu, X., Song, L., and Zhang, Y. (2019). Understandi ng real-world concurrency bugs in go. Proceedings of the Twenty-Fourth International Conference on Architectural Support for Programming Languages and Operating Systems

2019
[39]

Vafeiadis, V. (2011). Concurrent separation logic and o perational semantics. Electr. Notes Theor. Comput. Sci. , 276:335–351

2011
[40]

the i th transmission of the protocol speciﬁes that party P sends a message to party P ′ over channel c ∗

van Steen, M. and Tanenbaum, A. (2017). Distributed syst ems, 3rd ed. 51 Introduction Motivation Transforming Global Protocols so that Satisfying Implemen tations are FIFO Race-free Projections Verifying Towards Bug-Free Distributed Go Programs B.Comp. Dissertation Project ID:...

2017
[41]

Adve, S., Hill, M., Miller, B., and Netzer, R. (1991). Dete cting data races on weak memory systems. volume 19, pages 234–243

1991
[42]

Costea, M. A. (2017). A session logic for relaxed communic ation protocols

2017
[43]

Craciun, F., Kiss, T., and Costea, A. (2015). Towards a se ssion logic for communication protocols. In 2015 20th International Conference on Engineering of Complex Computer Systems (ICECCS) , pages 140–149. IEEE

2015
[44]

Garg, V. K. (2004). Concurrent and distributed computin g in java

2004
[45]

Hoare, C. (1969). An axiomatic basis for computer program ming. Commun. ACM , 12:576–580

1969
[46]

Honda, K., Yoshida, N., and Carbone, M. (2008). Multipar ty asynchronous session types. In Proceedings of the 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages , POPL ’08, page 273–284, New York, NY, USA. Association for Computing Machin ery

2008
[47]

Pike, R. (2012a). Concurrency is not parallelism

2012
[48]

Pike, R. (2012b). Go at google: Language design in the ser vice of software engineering

2012
[49]

The go memory model

The Go Authors (2014). The go memory model

2014
[50]

package ssa

The Go Authors (2020). package ssa

2020
[51]

Tu, T., Liu, X., Song, L., and Zhang, Y. (2019). Understa nding real-world concurrency bugs in go. Proceedings of the Twenty-Fourth International Conference on Architectural Support for Programming Languag es and Operating Systems

2019

Pith tools

Reviewed August 15, 2026 · model on record in the stance chip above.

[1] [1]

Adve, S., Hill, M., Miller, B., and Netzer, R. (1991). Detect ing data races on weak memory systems. volume 19, pages 234–243

work page 1991

[2] [2]

Bocchi, L., Demangeon, R., and Yoshida, N. (2012). A multi party multi-session logic. In TGC

work page 2012

[3] [3]

Brookes, S. (2007). A semantics for concurrent separati on logic. Theoretical Computer Science , 375(1):227–270. Festschrift for John C. Reynolds’s 70th bir thday

work page 2007

[4] [4]

and O’Hearn, P

Brookes, S. and O’Hearn, P. (2016). Concurrent separatio n logic. ACM SIGLOG News , 3:47–65

work page 2016

[5] [5]

and Pfenning, F

Caires, L. and Pfenning, F. (2010). Session types as intui tionistic linear propositions. In CONCUR

work page 2010

[6] [6]

Castro, D., Hu, R., Jongmans, S.-S., Ng, N., and Yoshida, N. (20 19). Distributed programming using role-parametric session types in go: Statically-typ ed endpoint apis for dynamically-instantiated communication structures. Proc. ACM Program. Lang. , 3(POPL)

work page

[7] [7]

Automated Verification of CountDownLatch

Chin, W., Le, T. C., and Qin, S. (2019). Automated veriﬁcati on of countdownlatch. ArXiv, abs/1908.09758

work page Pith review arXiv 2019

[8] [9]

Craciun, F., Kiss, T., and Costea, A. (2015). Towards a sess ion logic for communication protocols. In 2015 20th International Conference on Engineering of Complex Computer Systems (ICECCS) , pages 140–149. IEEE

work page 2015