From 6168f97d4f8db6dd3752494762f6d21be60c8956 Mon Sep 17 00:00:00 2001
From: Neven Villani <vanille@crans.org>
Date: Tue, 11 Mar 2025 10:21:18 +0100
Subject: [PATCH] Cleanup read_read_reorder and give it a README
---
theories/tree_borrows/README.md | 5 +-
.../tree_borrows/read_read_reorder/README.md | 32 ++++++
.../read_read_reorder/read_reorder.v | 105 ------------------
theories/tree_borrows/step_laws/steps_retag.v | 2 -
theories/tree_borrows/wishlist.v | 8 +-
5 files changed, 35 insertions(+), 117 deletions(-)
create mode 100644 theories/tree_borrows/read_read_reorder/README.md
diff --git a/theories/tree_borrows/README.md b/theories/tree_borrows/README.md
index 97bea348..833fff0a 100644
--- a/theories/tree_borrows/README.md
+++ b/theories/tree_borrows/README.md
@@ -27,10 +27,7 @@ Forked and adapted from the sibling folder `../stacked_borrows` with the same st
In addition, `read_read_reorder/` provides proofs of simple reorderings
(swapping adjacent operations in a sequential setting)
directly against the operational semantics.
-It is subdivided into
- * `equivalence_def.v`: definition of a simple notion of program equivalence for a sequential setting.
- * `low_level.v`: lemmas against the operational semantics.
- * `read_reorder.v`: actual proof of equivalence between two programs in which adjacent reads have been swapped. (Example 18)
+You can find more details in the associated `README.md`.
## Correspondence with Section 5
diff --git a/theories/tree_borrows/read_read_reorder/README.md b/theories/tree_borrows/read_read_reorder/README.md
new file mode 100644
index 00000000..39f1b8be
--- /dev/null
+++ b/theories/tree_borrows/read_read_reorder/README.md
@@ -0,0 +1,32 @@
+# Tree Borrows -- Read-read reorderings
+
+Example 18 focuses on the reordering of adjacent reads.
+We claim that Tree Borrows allows reordering of any two adjacent read accesses.
+The correctness of this optimization is trivial w.r.t. the state of the heap,
+but not so much w.r.t. the state of the trees of borrows.
+In fact this optimization is incorrect in Stacked Borrows!
+
+Our general framework is not at the moment capable of proving these optimizations because
+they require one of
+- absence of concurrency, or
+- ability to reason about data races.
+The latter has been demonstrated to be *possible* in simuliris (see `theories/simulang`),
+but combining this with Tree Borrows is outside of our current scope.
+Instead we opt for the former: this subdirectory has only sequential semantics,
+no concurrency.
+
+The main theorem for this proof is `read_reorder` in `read_reorder.v`,
+which states that the two example programs given that differ in the ordering
+of two reads are equivalent according to the notion defined in `equivalence_def.v`.
+In addition the intermediate lemmas in `low_level.v` should give confidence
+that this reordering is indeed a more general property of the model and not
+merely applicable to only this simple example.
+
+## Files
+
+In addition to the regular definitions of TB that are in the parent directory,
+this proof is subdivided into
+ * `equivalence_def.v`: definition of a simple notion of program equivalence for a sequential setting.
+ * `low_level.v`: lemmas against the operational semantics.
+ * `read_reorder.v`: actual proof of equivalence between two programs in which adjacent reads have been swapped. (Example 18)
+
diff --git a/theories/tree_borrows/read_read_reorder/read_reorder.v b/theories/tree_borrows/read_read_reorder/read_reorder.v
index 0cfc440c..a4f42a9c 100644
--- a/theories/tree_borrows/read_read_reorder/read_reorder.v
+++ b/theories/tree_borrows/read_read_reorder/read_reorder.v
@@ -162,30 +162,6 @@ Proof.
{ simpl. eapply base_prim_step.
econstructor 1. econstructor. 1: done. done. }
split; last done. rewrite bool_decide_decide decide_True //; congruence.
-(* - (* read x1: succeed, read x2: fail *)
- do 2 eexists. split.
- { change (Let x2 ?a ?b) with (fill [LetEctx x2 b] a).
- eapply fill_prim_step. eapply base_prim_step.
- econstructor 2. 1: econstructor 4. 1: done.
- econstructor.
- + eapply apply_read_within_trees_same_tags; eassumption.
- + eapply read_failure_preserved.
- * eexists. eexists. apply (Hwf.(state_wf_tree_compat _)).
- * eassumption.
- * eassumption.
- }
- do 2 eexists. split.
- { simpl. eapply base_prim_step.
- econstructor 1. econstructor. 1: done. done. }
- do 2 eexists. simpl. split.
- { change (Let x1 ?a ?b) with (fill [LetEctx x1 b] a).
- eapply fill_prim_step. eapply base_prim_step.
- econstructor 2. 1: econstructor 3. 1: done. simpl.
- econstructor; done. }
- do 2 eexists. split.
- { simpl. eapply base_prim_step.
- econstructor 1. econstructor. 1: done. done. }
- split; last done. rewrite bool_decide_decide decide_True //; congruence. *)
- (* read x1: zerosized, read x2: succeed *)
do 2 eexists. split.
{ change (Let x2 ?a ?b) with (fill [LetEctx x2 b] a).
@@ -222,86 +198,6 @@ Proof.
{ simpl. eapply base_prim_step.
econstructor 1. econstructor. 1: done. done. }
split; last by destruct σ. rewrite bool_decide_decide decide_True //; congruence.
-(* - (* read x1: zerosized, read x2: fail *)
- do 2 eexists. split.
- { change (Let x2 ?a ?b) with (fill [LetEctx x2 b] a).
- eapply fill_prim_step. eapply base_prim_step.
- econstructor 2. 1: econstructor 4. 1: done.
- econstructor; done. }
- do 2 eexists. split.
- { simpl. eapply base_prim_step.
- econstructor 1. econstructor. 1: done. done. }
- do 2 eexists. simpl. split.
- { change (Let x1 ?a ?b) with (fill [LetEctx x1 b] a).
- eapply fill_prim_step. eapply base_prim_step.
- econstructor 2. 1: econstructor 3. 1: done. simpl.
- econstructor; done. }
- do 2 eexists. split.
- { simpl. eapply base_prim_step.
- econstructor 1. econstructor. 1: done. done. }
- split; last by destruct σ. rewrite bool_decide_decide decide_True //; congruence.
- - (* read x1: fail, read x2: succeed *)
- do 2 eexists. split.
- { change (Let x2 ?a ?b) with (fill [LetEctx x2 b] a).
- eapply fill_prim_step. eapply base_prim_step.
- econstructor 2. 1: econstructor 3. 1: done.
- econstructor; done. }
- simpl.
- do 2 eexists. split.
- { simpl. eapply base_prim_step.
- econstructor 1. econstructor. 1: done. done. }
- do 2 eexists. simpl. split.
- { change (Let x1 ?a ?b) with (fill [LetEctx x1 b] a).
- eapply fill_prim_step. eapply base_prim_step.
- econstructor 2. 1: econstructor 4. 1: done. simpl.
- econstructor.
- + erewrite <- apply_read_within_trees_same_tags; eassumption.
- + erewrite <- read_failure_preserved.
- * eassumption.
- * eexists. eexists. apply (Hwf.(state_wf_tree_compat _)).
- * eassumption.
- }
- (* this admit needs the theorem saying that if it fails earlier, it fails also after the other read has succeeded *)
- do 2 eexists. split.
- { simpl. eapply base_prim_step.
- econstructor 1. econstructor. 1: done. done. }
- split; last by destruct σ. rewrite bool_decide_decide decide_True //; congruence.
- - (* read x1: fail, read x2: zerosized *)
- do 2 eexists. split.
- { change (Let x2 ?a ?b) with (fill [LetEctx x2 b] a).
- eapply fill_prim_step. eapply base_prim_step.
- econstructor 2. 1: econstructor 3. 1: done.
- econstructor; done. }
- do 2 eexists. split.
- { simpl. eapply base_prim_step.
- econstructor 1. econstructor. 1: done. done. }
- do 2 eexists. simpl. split.
- { change (Let x1 ?a ?b) with (fill [LetEctx x1 b] a).
- eapply fill_prim_step. eapply base_prim_step.
- econstructor 2. 1: econstructor 4. 1: done. simpl.
- econstructor; done. }
- do 2 eexists. split.
- { simpl. eapply base_prim_step.
- econstructor 1. econstructor. 1: done. done. }
- split; last by destruct σ. rewrite bool_decide_decide decide_True //; congruence.
- - (* read x1: fail, read x2: fail *)
- do 2 eexists. split.
- { change (Let x2 ?a ?b) with (fill [LetEctx x2 b] a).
- eapply fill_prim_step. eapply base_prim_step.
- econstructor 2. 1: econstructor 4. 1: done.
- econstructor; done. }
- do 2 eexists. split.
- { simpl. eapply base_prim_step.
- econstructor 1. econstructor. 1: done. done. }
- do 2 eexists. simpl. split.
- { change (Let x1 ?a ?b) with (fill [LetEctx x1 b] a).
- eapply fill_prim_step. eapply base_prim_step.
- econstructor 2. 1: econstructor 4. 1: done. simpl.
- econstructor; done. }
- do 2 eexists. split.
- { simpl. eapply base_prim_step.
- econstructor 1. econstructor. 1: done. done. }
- split; last by destruct σ. rewrite bool_decide_decide decide_True //; congruence. *)
Qed.
Lemma read_example_no_termination x1 x2 l1 tg1 sz1 l2 tg2 sz2 erest P σ :
@@ -333,5 +229,4 @@ Proof.
Qed.
-
Print Assumptions read_reorder.
diff --git a/theories/tree_borrows/step_laws/steps_retag.v b/theories/tree_borrows/step_laws/steps_retag.v
index 5ae3fb21..2b2626cb 100644
--- a/theories/tree_borrows/step_laws/steps_retag.v
+++ b/theories/tree_borrows/step_laws/steps_retag.v
@@ -21,8 +21,6 @@ Implicit Types l : loc.
Implicit Types f : fname.
-
-
(** ** Retags *)
Lemma tree_access_succeeds_heap_value σ b ak tg blk off sz :
diff --git a/theories/tree_borrows/wishlist.v b/theories/tree_borrows/wishlist.v
index e5ea6c2b..2e59c695 100644
--- a/theories/tree_borrows/wishlist.v
+++ b/theories/tree_borrows/wishlist.v
@@ -1,14 +1,10 @@
+(** Reexports that are so universal that not including them here would make the
+ size of every other Require Import list explode. *)
From iris.proofmode Require Export proofmode.
From simuliris.tree_borrows Require Export tree_access_laws tag_protected_laws loc_controlled_laws.
-From iris.base_logic.lib Require Import ghost_map.
From simuliris.base_logic Require Export gen_sim_prog.
From simuliris.simulation Require Export slsls.
-From simuliris.simulation Require Import lifting.
-From simuliris.tree_borrows Require Import tkmap_view.
From simuliris.tree_borrows Require Export defs class_instances.
-From simuliris.tree_borrows Require Import steps_progress steps_inv.
-From simuliris.tree_borrows Require Import logical_state inv_accessors.
-From simuliris.tree_borrows.trees_equal Require Import trees_equal_base random_lemmas.
From iris.prelude Require Import options.
--
GitLab