Skip to content

Ci/tree borrows

Neven Villani requested to merge ci/tree-borrows into master

Full proof that adjacent read accesses can be swapped in a sequential setting. This relies on

  • commutation: if in state s0 the sequence read1; read2; suceeds and results in state s1, then read2; read1; also goes from s0 to s1
  • persistencce: if in state s0 the access read1 succeeds and results in state s1, then read2 suceeds in s0 if and only if it suceeds in s1.

The resulting theorems are in theories/tree_borrows/read_reorder.v.

Will be merged when I fix the mangling.

Edited by Neven Villani

Merge request reports