From ec3e8cd9bf7b52597d579ca4b30d8575d83c70e1 Mon Sep 17 00:00:00 2001 From: Ralf Jung <jung@mpi-sws.org> Date: Fri, 15 Nov 2024 12:32:09 +0100 Subject: [PATCH] readme tweaks --- theories/tree_borrows/README.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/theories/tree_borrows/README.md b/theories/tree_borrows/README.md index 2579f9db..45d7947c 100644 --- a/theories/tree_borrows/README.md +++ b/theories/tree_borrows/README.md @@ -23,7 +23,7 @@ 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 - * `refinement_def.v`: definition of a bisimulation relation for a sequential setting. + * `refinement_def.v`: definition of a simple notion of program equivalence for a sequential setting. * `low_level.v`: lemmas against the operational semantics. * `refinement.v`: actual proof of bisimulation between two programs in which adjacent reads have been swapped. @@ -50,7 +50,7 @@ These proofs do not use the `simuliris` library, but instead they do a much simp This is because these proofs only hold for a non-concurrent language. We suspect that they also hold in a concurrent setting, but this would require data race reasoning, and thus we have not proven that. -Specifically, the extremely simple notion of "equivalence after a few steps" is in `refinement_def.v`. +Specifically, the simple notion of "equivalence after a few steps" is in `refinement_def.v`. The proof that the two reads can be reordered is in `read_reorder.v`. The file `low_level.v` contains low-level lemmas used in `read_reorder.v` -- GitLab