[Pitch] Create official comprehensive concurrency documentation and adopt related enhanced processes

Evolution Pitches
, ,
1

Create official comprehensive concurrency documentation and adopt related enhanced processes

  • Proposal: SE-NNNN
  • Authors: Jonathan Gilbert
  • Review Manager: TBD
  • Status: Pitched

Note: this is a formal rework of an earlier pitch.

Introduction

I propose that the Swift project create an official ConcurrencySemantics.md document (or similar) and adopts more rigorous processes around the proposal/PR/commit phase of concurrency changes.

Motivation

Last week I saw @jamieQ's thread, "Which subsystem is responsible for preventing this concurrency bug?" (#88002), which details a runtime crash in the concurrency system that should be impossible if our implementation was consistent. The bug came into existence because of two factors:

  1. 2022 PR (AKA "C-DropGA") created a scenario where it was deemed safe to drop the @G global actor qualifier. At the time, it was. However...
  2. Then SE-0430 created sending, apparently unaware of the exception where @G can be dropped.
  3. This opened a hole in the concurrency isolation barrier, leading to a situation where a strict Swift 6 codebase could still crash on a data race.

@jamieQ wanted to know "which subsystem is responsible for preventing this." My first reaction is, there should be a document that coherently answers this question. However, I could not find one.

Secondly, it occurred to me that the subsystem responsible for preventing this bug is really the human subsystem. The lack of the kinds of processes and documentation that I'm pitching here is part of what can enable such bugs to come into existence in the first place. We should not be playing "whack-a-mole" and "elephant-in-the-room" with concurrency at this point. The first step towards better human understanding is good documentation and rigorous processes.

Proposed solution

Last week I published a comprehensive documentation of all the formal requirements and features of Swift Concurrency along with an analysis of whether the requirements are satisfiable, and whether the present implementation is consistent with the requirements, as a whitepaper on GitHub here. (Now with PDF.)

Section 7 of the whitepaper makes several constructive recommendations that could become several individual pitches, hopefully not all from the same person.

The first recommendation is (Section 7.C1):

Write the normative semantics down, with requirement IDs

A living docs/ConcurrencySemantics.md in swiftlang/swift (or a TSPL "reference" companion) that states the requirements of §2 normatively, each with an ID, an owner (per §5.1's matrix), and a change log. Mechanics that make it stick rather than rot:

  • Every carve-out (C-DropGA and friends) is registered with its soundness side condition stated explicitly. The ledger is greppable; an SE proposal that changes any crossing mechanism must include a "carve-out audit" section, exactly as proposals today must include "source compatibility" and "ABI stability" sections. This is a template change to the evolution process -- nearly free, and it is the single measure that would have caught SE-0430 × C-DropGA at review time.
  • Diagnostics and suppression heuristics reference requirement IDs in code comments, so PartitionUtils.h's elisions would read "sound by R-SEND-2 assuming no sending operand (see ledger entry CO-7)" instead of a bare English sentence.

The proposed document would:

  • explain the formal requirements of the Swift concurrency system (section 2)
  • explain the central theorem of the system to help guide understanding of the components (section 3)
  • explain how each and every keyword, type, attribute, and macro maps to the requirements (section 4)
  • explain which subsystems of the compiler are responsible for enforcing which requirements (section 5)
  • provide a consistency and satisfiability analysis of the current system (section 6)
  • explain how the system is meant to coexist with pre-concurrency code (section 8)

Alternatives considered

N/A

9 Likes
[Meta Pitch] Add Comprehensive Formal Documentation & Change Process for Swift Concurrency
2

I didn't yet find the time to immerse myself fully with your document, but (having skimmed it a couple of days ago) I'd still like to say: well done on taking the time in putting this together! Any sort of improvements to documentation related to Swift Concurrency is sorely welcome.

One immediate feedback from my side is that the intended audience of this document is not really clear, or at least to me is a tad murky. The spec itself provides some useful beginner-friendly analogies, but at later points surfaces compiler engineering jargon and implementation details.

I wonder if it makes sense to decouple this into two separate deliverables: an approachable guide aimed at app developers and a normative reference aimed at compiler engineers and evolution reviewers? All in all: huge props and am curious to hear what other folks think.

EDIT: I'm pleasantly surprised to see that the document is now even more approachable than when last I looked at it 2-3 days ago!

3

Thanks Nikola, I reworked it based on some DM feedback to have the first few sections more approachable. The idea is to "tell the story" of what Swift Concurrency is all about from the cornerstone principle of data race safety using an analogy (here, the "rooms/building/couriers" analogy).

The idea here is not to suggest MY doc is the one we should use, but mostly at this stage, to simply figure out what general kind(s) of doc(s) we want to make and what level(s) they should target.

You're right that I moved the higher-level stuff to an appendix at the end. I'm open to that being in a separate document, or making it clearer that the is an advanced section at the end.

I'm personally a believer in having it all together and giving it to people straight, similar to how we have the advanced "Language Reference" section at the end of the primary documentation. People are really smart, they'll know it's not all meant to be digested in one reading (but there are those geniuses out there who will anyway, and that's good). I would have loved to have a guide like that with advanced info about how the compiler works, much earlier in my journey with Swift, though I'm not one of those geniuses. Appreciating the underpinnings in the compiler will help a lot of developers, at least to write better bug reports, and hopefully empower more contributions and write better code.

I'll see about a draft that separates them and another draft that keeps them together, so we can see what that would look like.

Note: once a general format for these is settled upon, then my intention would be to get the best writer we can find to refine this into a more professional level of document.

2 Likes