pith. sign in

arxiv: 1907.04005 · v1 · pith:NOQBFLVJnew · submitted 2019-07-09 · 💻 cs.LO

Handling localisation in rely/guarantee concurrency: An algebraic approach

Larissa A. Meinicke , Ian J. Hayes This is my paper

Pith reviewed 2026-05-25 00:12 UTC · model grok-4.3

classification 💻 cs.LO
keywords rely/guaranteelocalisationrefinement algebralocal variablesconcurrent programscompositional reasoningsynchronous algebra
0
0 comments X

The pith

A primitive localisation operator in a synchronous concurrent refinement algebra allows proofs of its properties including interactions with rely and guarantee conditions.

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

This paper extends the rely/guarantee method for concurrent programs by adding support for local variables through an algebraic approach. It introduces a localisation operator as a primitive in the refinement algebra, from which local variable blocks are defined. This enables the body of a local block to have parallel processes that share the local variables. The approach supports mechanisation by proving properties algebraically rather than using ad-hoc rules. A reader would care because it provides a uniform way to reason compositionally about shared-variable programs with local state.

Core claim

The paper claims that by extending the synchronous concurrent refinement algebra with a primitive localisation operator, local variable blocks can be defined, and properties of localisation, including its interaction with rely and guarantee conditions, can be proved from the algebra's foundations consisting of a small set of primitive commands and operators.

What carries the argument

The primitive localisation operator, which is used to define local variable blocks in the algebra.

If this is right

  • Local variable blocks can be defined using the localisation operator without additional rules.
  • Properties of localisation can be proved including interactions with rely and guarantee conditions.
  • The algebra supports compositional reasoning about concurrent programs with local variables.
  • All remaining constructs are defined from the small set of primitives.
  • Mechanisation of the rely/guarantee approach is facilitated.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • This algebraic treatment might allow similar localisation handling in other refinement-based concurrency frameworks.
  • Implementation in proof assistants could be simplified by the primitive-based definition.
  • Testing the algebra on examples with nested local variables could reveal further properties.
  • The method suggests localisation can be handled uniformly without special cases for parallel components.

Load-bearing premise

A small set of primitive commands and operators is sufficient to define all remaining constructs, including the localisation operator, without additional ad-hoc rules.

What would settle it

Finding a concurrent program with local variables where the interaction between localisation and rely/guarantee conditions cannot be proved using only the algebra's axioms would falsify the approach.

read the original abstract

The rely/guarantee approach of Jones extends Hoare logic with rely and guarantee conditions in order to allow compositional reasoning about shared-variable concurrent programs. This paper focuses on localisation in the context of rely/guarantee concurrency in order to support local variables. Because we allow the body of a local variable block to contain component processes that run in parallel, the approach needs to allow variables local to a block to become shared variables of its component parallel processes. To support the mechanisation of the rely/guarantee approach, we have developed a synchronous concurrent refinement algebra. Its foundation consists of a small set of primitive commands plus a small set of primitive operators from which all remaining constructs are defined. To support local variables we add a primitive localisation operator to our algebra that is used to define local variable blocks. From this we can prove properties of localisation, including its interaction with rely and guarantee conditions.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 3 minor

Summary. The paper develops a synchronous concurrent refinement algebra whose foundation is a small set of primitive commands and operators. To handle local variables in rely/guarantee reasoning it introduces one new primitive localisation operator used to define local-variable blocks; the claim is that all other constructs, including the interaction of localisation with rely and guarantee conditions, can then be derived algebraically.

Significance. If the derivations hold, the work supplies a compact algebraic basis that could support mechanised proofs of rely/guarantee properties for programs containing local variables that become shared among parallel components. The emphasis on a minimal primitive set and the explicit construction of localisation are positive features for reproducibility and mechanisation.

minor comments (3)
  1. [Abstract / Introduction] The abstract asserts that properties 'can be proved' from the algebra; the introduction or an early section should contain at least one fully expanded derivation (with each step justified by a named axiom or definition) so that readers can verify the claimed reduction to the primitive basis.
  2. [Section introducing the localisation operator] Notation for the new localisation operator and its interaction with parallel composition should be introduced with an explicit equational definition (e.g., an equation number) before any properties are stated.
  3. [Foundational definitions] A short table or list enumerating which constructs are primitive versus which are derived would make the 'small set of primitives' claim easier to assess.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the supportive summary, the recognition of the algebraic approach, and the recommendation of minor revision. The report lists no specific major comments.

Circularity Check

0 steps flagged

No significant circularity identified

full rationale

The paper constructs a synchronous concurrent refinement algebra from an explicitly stated small set of primitive commands and operators, introduces one new primitive (localisation) to define local variable blocks, and derives properties of localisation and its interactions with rely/guarantee conditions directly from those algebraic definitions. No equation or property is shown to reduce by construction to a fitted parameter, a self-referential definition, or a load-bearing self-citation chain; the derivations remain independent of the target results.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 1 invented entities

The central claim rests on the existence of a small primitive basis from which localisation and its laws are derived; the abstract does not list explicit axioms beyond the standard algebraic setting.

axioms (1)
  • domain assumption A small set of primitive commands and operators forms a sufficient foundation for all remaining constructs including localisation.
    Explicitly stated in the abstract as the basis of the algebra.
invented entities (1)
  • localisation operator no independent evidence
    purpose: Defines local variable blocks and allows local variables to become shared among parallel component processes.
    New primitive added to the algebra specifically to support localisation.

pith-pipeline@v0.9.0 · 5675 in / 1201 out tokens · 24420 ms · 2026-05-25T00:12:17.556068+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

18 extracted references · 18 canonical work pages

  1. [1]

    Fixed-point calculus

    Chritiene Aarts, Roland Backhouse, Eerke Boiten, Henk Do ombos, Netty van Gasteren, Rik van Geldrop, Paul Hoogendijk, Ed V oermans, and Jaap van der Woude. Fixed-point calculus. 16 L. A. Meinicke and I. J. Hayes Information Processing Letters , 53:131–136, 1995. Mathematics of Program Construction Group

    work page 1995

  2. [2]

    P . H. G. Aczel. On an inference rule for parallel com- position, 1983. Private communication to Cliff Jones http://homepages.cs.ncl.ac.uk/cliff.jones/publications/MSs/PHGA-traces.pdf

    work page 1983

  3. [3]

    J. W. Coleman and C. B. Jones. A structural proof of the soun dness of rely/guarantee rules. Journal of Logic and Computation , 17(4):807–841, 2007

    work page 2007

  4. [4]

    R. J. Colvin, I. J. Hayes, and L. A. Meinicke. Designing a se mantic model for a wide- spectrum language with concurrency. F ormal Aspects of Computing, 29:853–875, 2016

    work page 2016

  5. [5]

    de Roever

    W.-P . de Roever. Concurrency V erification: Introduction to Compositional and Noncompo- sitional Methods. Cambridge University Press, 2001

    work page 2001

  6. [6]

    J. Dingel. A refinement calculus for shared-variable para llel and distributed programming. F ormal Aspects of Computing, 14(2):123–197, 2002

    work page 2002

  7. [7]

    Hayes, and Andrius V elykis

    Julian Fell, Ian J. Hayes, and Andrius V elykis. Concurren t refinement al- gebra and rely quotients. Archive of F ormal Proofs , December 2016. http://isa-afp.org/entries/Concurrent_Ref_Alg.shtml, Formal proof development

    work page 2016

  8. [8]

    I. J. Hayes, R. J. Colvin, L. A. Meinicke, K. Winter, and A. V elykis. An algebra of syn- chronous atomic steps. In J. Fitzgerald, C. Heitmeyer, S. Gn esi, and A. Philippou, editors, FM 2016: F ormal Methods: 21st International Symposium, Pro ceedings, volume 9995 of LNCS, pages 352–369, Cham, November 2016. Springer Internation al Publishing

    work page 2016

  9. [9]

    Hayes, Larissa A

    Ian J. Hayes, Larissa A. Meinicke, Kirsten Winter, and Rob ert J. Colvin. A synchronous program algebra: a basis for reasoning about shared-memory and event-based concurrency. F ormal Aspects of Computing, 31(2):133–163, April 2019

    work page 2019

  10. [10]

    Cylindric Algebras, Part I., volume 64 of Studies in logic and the foundations of mathematics

    Leon Henkin, James Donald Monk, and Alfred Tarski. Cylindric Algebras, Part I., volume 64 of Studies in logic and the foundations of mathematics . North-Holland Pub. Co., 1971

    work page 1971

  11. [11]

    C. A. R. Hoare, B. M¨ oller, G. Struth, and I. Wehrman. Conc urrent Kleene Algebra and its foundations. J. Log. Algebr . Program., 80(6):266–296, 2011

    work page 2011

  12. [12]

    C. B. Jones. Development Methods for Computer Programs including a Noti on of Interfer- ence. PhD thesis, Oxford University, June 1981. Available as: Ox ford University Computing Laboratory (now Computer Science) Technical Monograph PRG -25

    work page 1981

  13. [13]

    C. B. Jones. Specification and design of (parallel) progr ams. In Proceedings of IFIP’83 , pages 321–332. North-Holland, 1983

    work page 1983

  14. [14]

    C. B. Jones. Tentative steps toward a development method for interfering programs. ACM ToPLaS, 5(4):596–619, 1983

    work page 1983

  15. [15]

    The rely-guarantee method in Isabe lle/HOL

    Leonor Prensa Nieto. The rely-guarantee method in Isabe lle/HOL. In Proceedings of ESOP 2003, volume 2618 of LNCS. Springer-V erlag, 2003

    work page 2003

  16. [16]

    Prisacariu

    C. Prisacariu. Synchronous Kleene Algebra. Journal of Logic and Algebraic Programming , 79(7):608–635, 2010

    work page 2010

  17. [17]

    von Wright

    J. von Wright. Towards a refinement algebra. Science of Computer Programming, 51:23–45, 2004

    work page 2004

  18. [18]

    The rely- guarantee method for verifying concurrent programs

    Qiwen Xu, Willem-Paul de Roever, and Jifeng He. The rely- guarantee method for verifying concurrent programs. F ormal Aspects of Computing, 9:149–174, 1997

    work page 1997