Lawyer and its wait-freedom extension

Overview

This repository contains the Rocq formalization for two related papers:

1. "Lawyer: Modular Obligations-Based Liveness Reasoning in Higher-Order Impredicative Concurrent Separation Logic", OOPSLA'26 - a program logic for proving (un)fair termination of concurrent higher-order programs.
2. "Verifying wait-freedom for concurrent higher-order programs", ECOOP'26 - extends Lawyer to establish wait-freedom of concurrent higher-order programs.

The wait-freedom development is built as an extension of the Lawyer project. Both rely on Trillium framework; however, the wait-freedom extension requires a fork of Trillium (namely, its' trillium_wfree branch) with a generalized adequacy theorem and weakest precondition; the Lawyer development still works with that fork. This document describes both developments together, since most of the Rocq implementation is shared.

There are also artifacts available for each of the papers:

• https://zenodo.org/records/19181284
• https://zenodo.org/records/20134905

Structure of the technical development

• fairness/ - general definitions of traces and fairness, as well as various utility files
• heap_lang/ - definition and reasoning rules for the programming language being used
• lawyer/
  • examples/ - case studies for Lawyer
  • obligations/ - implementation of the obligations-based reasoning
  • nonblocking/ - wait-freedom extension of Lawyer. Most of it resides in this folder directly, except for:
    • tokens/ - adaptation to the restricted wait-freedom
    • logrel/ - definitions and theorems about logical relations
    • examples/ - case studies on wait-freedom
• check/ - collection of the end results
  • check.v - end results for Lawyer
  • check_wfree.v - end results for the wait-freedom extension

Installation

First, install opam according to the instructions for your operating system. We used the version 2.1.2.

Then clone the sources into lawyer folder.

Then execute the following.

# create a new opam environment
opam switch create lawyer-env 5.4.0
# switch into the new environment
eval $(opam env --switch=lawyer-env)

# set up repository for Rocq packages
opam repo add coq-released https://coq.inria.fr/opam/released
# set up repository with the Trillium extension
opam repo add logsem-opam https://github.com/logsem/opam

# move into the Lawyer directory
cd lawyer/
# install all dependencies of Lawyer
opam install . --deps-only
# build Lawyer; adjust the number of jobs as needed
make -j 5

Checking the end results

1. Build the project as described above.

2. Open check/check.v for Lawyer results, or check/check_wfree.v for wait-freedom results, with an editor of choice. In each file, the definition results is a tuple collecting the proofs of progress properties of all corresponding case studies.

3. Step through every line of this file.

4. The last Print Assumptions line prints all the axioms that the listed theorems rely on. Processing it might take a while.

   The used axioms will be listed at the bottom of the output. Check that only the following axioms are used:

   • RelationalChoice.relational_choice
   • ClassicalUniqueChoice.dependent_unique_choice
   • Classical_Prop.classic
   • classical.PropExt
   • classical.FunExt
   • classical.Choice

Correspondence between the paper and Rocq formalization

Lawyer

Section 2

Section 2.1

• No-Obligations Model (Fig. 1) It can be viewed simply as a subset of the Obligations Model with restricted state and transitions. Namely, No-Obligations Model corresponds to choosing Level to be the empty set (see Appendix C). Therefore, we do not provide a separate Rocq definition of No-Obligations Model.

• Example programs Each example program from Section 2.1 has a subfolder X in lawyer/examples/. Inside of it, the X.v file contains the verification of the program, and X_adequacy.v proves the meta-level property about the execution of that program.

  • Statically-known bound (Fig. 2): const_term/subfolder. The proved property is execution time being linear wrt. the value of N argument.
  • Runtime-determined Bound (Fig. 3): rt_bound/ subfolder. The proved property is termination under fair scheduler (since internally it uses a blocking nondet function).
  • Delaying example (Fig. 4): lf_counter/ subfolder. The proved property is termination under any scheduler.

Section 2.2

• Definition of Obligations Model (Fig. 5): lawyer/obligations/obligations_model.v
  • OM parameters: ObligationsParams typeclass
  • OM state: ProgressState record. Note that "fuel" component of the state is named "ps_cps", and the "barrel" resource in logic is called "cp". Well-formedness condition is defined in lawyer/obligations/obligations_wf.v, record om_st_wf.
  • OM transitions: definition om_trans
  • OM as a Trillium model: definition ObligationsModel
• Example programs Similarly to the above, the results are located in the subfolders of lawyer/examples/. The property we prove for these examples is termination under fair scheduler.
  • Blocking example (Fig. 6): nondet/ subfolder, see specifically nondet/nondet_adequacy.v, theorem nondet_pre_allocated_termination.
  • Fork example (Fig. 7): nondet/ subfolder.

Section 2.3

• General trace-related definitions: defined in the Trillium fork; see the README.md in it

• Operational semantics of our language (Fig. 8): heap_lang/lang.v

• Refinement relation (definitions 1, 2 and 3). Our implementation of refinement proceeds slightly differently compared to the paper presentation.

  1. The state relation in paper (Definition 1) consists of two parts: sameThreads and liveThreads. Contrary, the Rocq version (lawyer/obligations/obligations_adequacy.v, definition obls_st_rel) only includes the latter. Indeed, sameThreads is not explicitly used for proving termination, which is the main purpose of the refinement we establish. However, sameThreads is used to establish the refinement (lawyer/obligations/obligations_adequacy.v, proof of lemma no_obls_live_tids) as a part of proving AlwaysHolds. Therefore, we keep this condition as a part of trace interpretation (see lawyer/obligations/obligations_em.v, definition threads_own_obls).
  2. The finite trace refinement in paper (Definition 2) is defined by placing restrictions on every transition in both traces. Contrary, the Rocq implementation proceeds in two steps.
     1. We start by defining the notion of "valid evolution step" (lawyer/obligations/obligations_em.v, definition obls_valid_evolution_step) that intuitively captures the "lock-step" relation between physical and model steps.
     2. Then, we show that the proof of weakest precondition implies intensional refinement (see Trillium paper for definition) of the specific relation on pairs of physical and model traces. Namely, the last transitions of such traces must form a valid evolution step.
     3. Then, we show that this intensional refinement in fact implies the refinement from Definition 3 (minus the sameThreads part discussed above).

  See heap_lang/simulation_adequacy.v, comment inside of strong_simulation_adequacy_traces_multiple lemma that discusses points 2 and 3 above.

• Relative image-finiteness of refinement relation (Lemma 2.1): lawyer/obligations/obligations_adequacy.v, lemma obls_sim_rel_FB.

• General trace fairness (definition 4): fairness/fairness.v, definition fair_by'. Also see the lemma fair_by'_weakly_fair in the same file for equivalence with more common notion of weak fairness. Then, notion of fair execution is given by fair_ex. "Obligations-fair" traces are defined in lawyer/obligations/obligations_model.v, definition obls_trace_fair.

• Transporting of execution fairness to the model trace (Lemma 2.2): lawyer/obligations/obligations_adequacy.v, lemma exec_om_fairness_preserved

• Termination of obligations-fair OM traces (Lemma 2.3): lawyer/obligations/obls_termination.v, theorem obls_fair_trace_terminate

Section 3

• Verification of nondet example: lawyer/examples/nondet/nondet.v
• Definitions of OM resources (Fig. 9), OU (along with its iterated version) and related lemmas (Fig. 10): lawyer/obligations/obligations_resources.v
• Two-step program logic and model updates: lawyer/program_logic.v. In particular, the rule trillium-step-nval-simpl corresponds to the lemma sswp_MU_wp.
• sswp and rules for it: lawyer/program_logic.v (adapted from Fairneris project): heap_lang/sswp_logic.v

Section 4

The case study is located in lawyer/examples/ticketlock/. Code for ticketlock implementation and top-level program can be found inn ticketlock.v and client.v correspondingly. The final result stating the fair termination of the closed program is located in closed_adequacy.v.

Section 4.1

• BOU definition and related lemmas (Fig. 14): see lawyer/obligations/obligations_resources.v.
• The rule MU-OM-nofork: lawyer/obligations/obligations_logic.v, lemma BOU_AMU. Throughout the development, we use the AMU modality, which can be thought of as simply MU.

Section 4.2

• Sequential fair lock specification (Fig. 15): lawyer/examples/ticketlock/releasing_lock.v, record ReleasingFairLock.

Section 4.3

• Proof that ticketlock satisfies the sequential lock specification for any choice of spec's parameters satisfying a number of restrictions: lawyer/examples/ticketlock/ticketlock_releasing.v, definition RFL_FL_TL'.
• Verification of ticketlock implementation against the logically atomic specification: lawyer/examples/ticketlock/ticketlock.v, see in particular TL_FL.
• Derivation of the sequential specification for a wrapper over logically atomic implementation: lawyer/examples/ticketlock/releasing_lock.v, see in particular RFL_FL.

Section 4.4

Verification of the top-level program on top of the sequential lock specification: lawyer/examples/ticketlock/client.v, theorem client_spec.

Appendix

Appendix A

• Well-formedness of obligations states: lawyer/obligations/obligations_wf.v, record om_st_wf.
• OM starting state (definition 6): lawyer/obligations/obligations_em.v, definition init_om_state.

Appendix B

• Full adequacy theorem of Lawyer: lawyer/obligations/obligations_adequacy.v, lemma obls_terminates_impl_multiple.
• Specialized adequacy theorem (Theorem B.1): lemma obls_terminates_impl_paper.

Appendix C

• Termination of all OM traces when Level is the empty set (Corollary C.1): lawyer/obligations/unfair_termination.v, lemma always_term_wo_lvls.
• Termination within constant time when Level is the empty set and Degree is singleton (Corollary C.2): lawyer/obligations/unfair_termination.v, lemma always_terminates_within_bound.

Appendix D

Operational semantics of our language (Fig. 8 and 16): heap_lang/lang.v. The mechanization mentions prophecy variables, but they are never used throughout the development.

Appendix E

Full form of Lawyer rules (Fig. 17) can be found in lawyer/program_logic.v (rules connecting wp with sswp and MU) and lawyer/obligations/obligations_logic.v (rules connecting MU with BOU).

Appendix F

• "Total" atomic updates (Definition 7): lawyer/examples/ticketlock/obls_atomic.v, definition TAU.
• "Total" logically atomic triples: lawyer/examples/ticketlock/obls_atomic.v, definitions TLAT and TLAT_RR for different kinds of "wait clauses" used in underlying TAU
• Logically atomic fair lock specification (Fig. 18): lawyer/examples/ticketlock/fair_lock.v, record FairLock.

Appendix G

Verification of the top-level program on top of the sequential lock specification: lawyer/examples/ticketlock/client.v, theorem client_spec.

Additional case studies

• Two implementations of parallel composition operator and rules for them: lawyer/examples/par.v, definitions par and par_sym, along with par_spec and par_sym_spec lemmas. Moreover, the case study in lawyer/examples/nondet/(nondet_par.v, nondet_par_adequacy.v) is a version of nondet implementation that uses parallel composition.
• A program consisting of two threads that increment the shared counter in turns, up to a certain bound, waiting for each others' turn: lawyer/examples/eo_fin/(eo_fin.v, eo_fin_adequacy.v)
• Program illustrating the concurrent use of two locks: lawyer/examples/ticketlock/(two_locks, two_locks_adequacy).v

Wait-freedom extension

Section 2

• General definitions and lemmas about traces: trillium/traces/*.v

Section 2.1

• Operational semantics of our language (Figure 3): heap_lang/lang.v
• Calls and returns (Definition 1): lawyer/nonblocking/trace_context.v, definitions call_at and return_at
  Note that the former explictly mentions the call argument, whereas the definition in the paper existentially quantifies over it.
• Eventual return of calls (Definition 2): lawyer/nonblocking/wfree_traces.v, definition always_returns_strong
  Note that it is additionally parameterized with:
  • stuckness bit (thus covering the possibly-stuck definition)
  • predicate on the call argument. This parameter is always set to an always true predicate and thus can be ignored.
• Call fairness ("schedUntilRet"): lawyer/nonblocking/wfree_traces.v, definition fair_call_strong
• Client validity: lawyer/nonblocking/logrel/valid_client.v, definition valid_client
• Wait-freedom (Definition 3): lawyer/nonblocking/wfree_traces.v, definition wait_free_strong
  Again, it is parameterized by a stuckness bit and an unused predicate on call arguments.

Section 2.2

• Lawyer specification of wait-freedom (Definition 4): lawyer/nonblocking/om_wfree_inst.v, record WaitFreeSpec
  Note the following:
  • This specification explicitly mentions an invariant that should be established from the starting configuration and which is assumed by both Hoare triples.
    In contrast, Definition 4 does not mention a module invariant explicitly and rather allows to take a viewshift from starting configuration before proving the Hoare triples.
    However, viewshifts allow establishing invariants, and the proofs in the paper (Sec. 4) proceed exactly by establishing a module invariant.
    See Iris Lecture Notes, Sec 4.3 "Abstract Data Types" for the discussion on these specification styles.
  • Parameter P can be ignored
  • The amount of fuel consumed by the operation is determined by the fuel function wfs_F, mentioned in Sec. 5.1
  • We prohibit the wait-free operation from forking using the forking bit. For that, we use our variation of Trillium weakest precondition defined in trillium/bi/weakestpre.v.
• Wait-freedom adequacy theorem (Theorem 5): lawyer/nonblocking/wfree_adequacy.v, theorem wfree_is_wait_free
  Again, it is parameterized by a stuckness bit, and the unused predicate on call arguments is set to be always true.
  It also explicitly requires the value representing the wait-free operation to be a lambda-expression.

Section 3

We do not mechanize the proofs presented in this section, as they are only used for explaining the Iris logic and not for establishing wait-freedom of incr (which is done in Section 4).
The specifications and proofs are standard and explained in e.g., Iris Lecture Notes.

Section 4

• Verification of the wait-freedom specification for the counter example:
  lawyer/nonblocking/examples/counter/counter.v, definition counter_WF_spec
  Note that we use the two-step logic of Lawyer to verify the Lawyer triples.
  In this logic, verifying every step amounts to applying two rules: one for the physical execution step and one for the model step.
  The former rules (e.g. wp_faa) are listed in heap_lang/sswp_logic.v, whereas the latter are implicitly applied by tactics such as MU_by_burn_cp.
• Wait-freedom of counter example: lawyer/nonblocking/examples/counter/counter_adequacy.v
• The degree parameter of fuel is always set to the lowest degree d0 of our Obligations Model instantiation: see wfs_spec in WaitFreeSpec located in lawyer/nonblocking/om_wfree_inst.v
• The fraction parameter of phase is always set to 1/2: see the Hoare triple in wait_free_method_gen located in lawyer/nonblocking/om_wfree_inst.v
• NoInfExec Lawyer triple for wait-freedom: lawyer/nonblocking/om_wfree_inst.v, definition wait_free_method_gen
  Ignore the P and Q parameters.
• PresInv triple for wait-freedom: defined directly as value interpretation (see Sec. 6.2)

Section 5

Section 5.1

• Stuckness variations of definitions related to wait-freedom (Definitions 6 and those mentioned below it): they are specific cases of definitions used for Section 2.1 with stuckness bit set to MaybeStuck.

• Adequacy theorem for possibly-stuck wait-freedom: instantiation of lawyer/nonblocking/wfree_adequacy.v, theorem wfree_is_wait_free with stuckness bit set to MaybeStuck.

• Modular verification of list_map: lawyer/nonblocking/examples/list_map/list_map.v

  • list_map implementation (Figure 6a): hl_list_map_cur.
  • Modular proof of specification: hlm_WF_fix_spec_unsafe. Note that we verify wait-freedom for eta-expanded hl_list_map_cur f due to the lambda-expression restriction (mentioned above).

• Possibly-stuck wait-fredom of list_map (incr l):

  lawyer/nonblocking/examples/list_map/list_map_adequacy.v.

• Fuel function: wfs_F component of WaitFreeSpec.

Section 5.2

Note that throughout the restricted wait-freedom development we use multisets of operations instead of lists.

• Implementation of the queue algorithm (Figure 7) in our language is scattered across multiple files in lawyer/nonblocking/examples/queue:

  • dequeuer/dequeue.v, definition dequeue
  • dequeuer/read_head_dequeuer.v, definition read_head_dequeuer
  • dequeuer/dequeuer_thread.v, definition dequeuer_thread
  • enqueuer/enqueue.v, definition enqueue
  • enqueuer/read_head.v, definition read_head_enqueuer
  • enqueuer/enqueuer_thread.v, definition enqueuer_thread

• Restricted wait-freedom (Definition 7): lawyer/nonblocking/wfree_traces.v, definition wait_free_restr.

• Exclusion of forks: lawyer/nonblocking/logrel/valid_client.v, definition no_forks.

• Specification of restricted wait-freedom (Definition 8):

  lawyer/nonblocking/tokens/om_wfree_inst_tokens.v, definition WaitFreeSpecToken.

• Definition and lemmas about tokens resource algebra: lawyer/nonblocking/tokens/tokens_ra.v

• Adequacy theorem for restricted wait-freedom (Theorem 9):

  lawyer/nonblocking/tokens/wfree_adequacy_tokens.v, theorem wfree_token_is_wait_free_restr.

• Restricted wait-freedom of the queue algorithm:

  lawyer/nonblocking/examples/queue/simple_queue_adequacy.v

Section 6

Section 6.1

• Reduction to proving termination: it is scattered across multiple lemmas used to prove wfree_is_wait_free mentioned above.
  In particular, see the lemmas in WFAdequacy section which fixes the parameters of an infinite call.

• Definition of progress resource: trillium/trillium/program_logic/adequacy_cond.v, record ProgressResource. Note that it is additionally parameterized with stuckness and forking bits (and list of postconditions mentioned in the appendix).

• Conditional adequacy theorem of Trillium (Theorem 10):

  trillium/trillium/program_logic/simulation_adequacy_em_cond.v,

  theorem PR_strong_simulation_adequacy_traces_multiple.

• Refinement relation for wait-freedom: lawyer/nonblocking/wfree_adequacy_lib.v, definition obls_sim_rel_wfree

Section 6.2

• Expression relation: lawyer/nonblocking/logrel/logrel.v, definition interp_expr
• Value relation (Definition 11): lawyer/nonblocking/logrel/logrel.v, definition interp
• Fundamental theorem (Theorem 12): lawyer/nonblocking/logrel/fundamental.v, theorem fundamental
• Robust safety of the wait-free operation (Theorem 13): lawyer/nonblocking/wfree_adequacy.v, definition init_wptp_wfree

Section 6.3

• Definition of progress resource for wait-fredom: lawyer/nonblocking/pr_wfree.v, definition pr_pr_wfree.
• Definition of the infCallPrefix predicate: lawyer/nonblocking/wfree_traces.v, definition fits_inf_call.
• Proof of the progress resource laws: lawyer/nonblocking/pr_wfree.v, definition PR_wfree.

Extra

• "Wait-freedom" of a simple sequential program: lawyer/nonblocking/examples/mk_ref/(mk_ref, mk_ref_adequacy).v
• Variations of above definitions and theorems for restricted wait-freedom: lawyer/nonblocking/tokens/*.v.
  In particular:
  • Extension of trace intepretation for physical WP that keeps track of method tokens: pwp_ext.v
  • Logical relation and fundamental theorem for token-based specifications: logrel_tok.v and fundamental_tok.v
  • Lifting of a stronger specification to one required by token-based FTLR: op_spec_lifting.v, lemma lift_spec
  • Progress resource for restricted wait-freedom: pr_wfree_tokens.v