Overview

This project is the companion Rocq development of the paper "A Separation Logic for Parallel Time Complexity with Work and Span Credits".

Setup & Build

See INSTALL.md.

Architecture

Rocq files are located in the src/ directory.

• directory lang contains the syntax and semantics of the language we study:
  • syntax is in syntax.v and syntax_instances.v
  • the head reduction relation is in head_semantics.v
  • the scheduler and main reduction relation are in semantics.v
• directory logic contains the program logic:
  • wpg.v defines the general weakest precondition wpg and its structural rules
  • wp.v defines the single-thread WP wp as a special case of wpg
  • wp_logatom.v defines logically atomic WP triples
  • interp.v defines the ghost state, the state interpretation predicate, and the work/span credit assertions
  • adequacy.v contains the soundness theorem
• directory examples contains the case studies
• directory utils contains utility functions and lemmas

Links with the Paper

Rocq files are located in the src/ directory. Work credits are called wcredits and span credits scredits.

• Figures 1 and 4 (the small example): in examples/small.v

• Figure 2 (Reasoning rules for credits, and for the tick and the parallel primitives):

  • Tick: wp_tick in logic/wp.v
  • Transfer: wp_transfer in logic/wp.v
  • Par: wp_par in logic/wp.v

• The WorkSplit and SpanSplit rules (inline in Section 2, not in a figure):

  • WorkSplit: wcredits_split in logic/interp.v
  • SpanSplit: scredits_split in logic/interp.v

• Figure 5 (Syntax of ParLang):

  • values and expressions are defined in lang/syntax.v, types val and expr
  • evaluation contexts are in lang/syntax.v, type ctx

• Figure 6 (Head reduction relation):

  • the head reduction relation is defined in lang/head_semantics.v

• Figure 7 (Reduction under a context and parallelism):

  • the task tree is defined in lang/semantics.v, type task_tree
  • the computation graph fork and join operations are graph_fork and graph_join in lang/semantics.v
  • the scheduler step relation is sched_step in lang/semantics.v
  • the main step relation is step in lang/semantics.v

• Figure 8 (Reasoning rules for base constructs), in logic/wp.v

• Figure 9 (Reasoning principles for the Transfer rule):

  • the transferable relation is defined in logic/transferable.v
  • isfork and isjoin are defined in logic/interp.v
  • GenerateTransferable: wp_transferable in logic/wp.v
  • PrimitiveTransfer: wp_primitive_transfer in logic/wp.v
  • End: wp_end in logic/wp.v

• Figure 10 (Definitions of the WorkBound and SpanBound predicates):

  • work_bounded in logic/adequacy.v
  • path (inductive definition of a weighted path) in logic/adequacy.v
  • span_bounded in logic/adequacy.v

• Figure 11 (Reducibility and safety of a configuration):

  • reducible is defined in lang/reducible.v
  • Safe is called adequate defined in logic/adequacy.v

• Theorem 4.1 (Soundness of the program logic):

  • stated and proved as wp_adequacy in logic/adequacy.v

• Figure 12 (Definition of the weakest precondition):

  • the general WP wpg is defined as the fixpoint of wpg_pre in logic/wpg.v
  • the single-thread WP wp is defined in logic/wp.v

• Figure 13 (Definition of the state interpretation predicate):

  • the state interpretation predicate is interp in logic/interp.v
  • winterp (coupling of pureinv and interp) is in logic/wpg.v

• Figure 14 (Definition of pure invariants):

  • the compatibility predicate comptree is defined inductively in logic/pureinv.v
  • the pure invariant pureinv is defined as a record in logic/pureinv.v

• Figures 15 and 16 (Ghost state for work credits, and ghost state for span credits): in logic/interp.v.

• Figure 17 (The parallel for loop and its specification): in examples/parfor.v

• Figure 18 (The tabulate primitive, the scan function, and their specifications):

  • tabulate in examples/tabulate.v
  • scan in examples/scan.v

• Figure 19 (The parallel merge operation and its specification):

  • slices in examples/slice.v
  • sequential merge in examples/merge_seq.v
  • binary search in examples/binsearch.v
  • parallel merge in examples/merge.v. The closed forms are in examples/merge_closed.v.

• Figure 20 (The parallel merge sort and its specification): in examples/merge_sort.v.

• Figure 21 (Code and specifications for Treiber's stack): in examples/stack.v. Atomic triples are defined as atomic_wp and the ATRIPLE notation in logic/wp_logatom.v

Evaluation Instructions

Users can check that all files compile and that no Admitted or Axiom remains. It suffices to open the file src/noaxioms.v and play with it interactively. If the Rocq command Print Assumptions xxx prints "Closed under the global context", it indicates that xxx has no dependencies (reference). Some case studies suppose the axiom functional_extensionality_dep due to the Equations plugin.

Users can also open some selected .v files inside RocqIDE or Proof General and evaluate the whole file to check that no errors occur and to verify that the objects and statements mentioned in the claims are what they are supposed to be.

ProofGeneral

NB: There is a hack to work with ProofGeneral. We have a dumb src/_CoqProject which makes visible the files produced by dune.

See issue: ProofGeneral/PG#477