TLA + specification of PCR parallel programming pattern
summary
Formalizes the Produce-Consume-Reduce parallel skeleton as a family of TLA+ modules and models concrete examples (fibPrimes1 and fibPrimes2) with nested PCRs and multidimensional index contexts, proving that the nested version implements the flat spec via a refinement mapping. Uses TLC and TLAPS for analysis: TLC model checks correctness, termination and refinement on small instances, TLAPS proves type invariants. Builds a translator plan from PCR syntax to TLA+ but notes missing features (iterate/feedback loops, early termination) and scalability limits for large state spaces.
AI-written summary · about
chapters (5)
- 0:00Introduction and agenda
- 2:16PCR pattern overview
- 17:14TLA+ specification overview
- 27:49Correctness and refinement
- 30:24Model checking and future work
related talks
01h 12mWorkshop: TLA+ in action (Part 4)
01h 14mWorkshop: TLA+ in action (Part 1)
01h 13mDesigning distributed systems with TLA+
14mPerformance Interfaces for Hardware Accelerators
01h 13mWorkshop: TLA+ in action (Part 3)
41mDesigning software with complex configurations
01h 11mWorkshop: TLA+ in action (Part 2)
15mTLC: Temporal Logic of Distributed Components