Sequentialisation proceedings #32
Conversation
There was a problem hiding this comment.
Pull Request Overview
This PR introduces foundational support for sequentialisation transformations by adding preservation lemmas in the core stepping operations, stubbing out sequentialisation proofs, and integrating a new src/sequentialization directory into the build.
- Added
guided_thrd_preserveandreex_thrd_preservelemmas to prove that thread sets remain unchanged. - Commented out
reexec_embd_tidincommit_embeddedand expanded sequentialisation modules with admitted proofs undersrc/sequentialization. - Updated the Makefile to include the new directory and cleaned up VSCode file-exclude settings.
Reviewed Changes
Copilot reviewed 11 out of 11 changed files in this pull request and generated 3 comments.
Show a summary per file
| File | Description |
|---|---|
| src/xmm/StepOps.v | Added two lemmas proving thread-set preservation for step ops. |
| src/xmm/Core.v | Commented-out record field reexec_embd_tid in commit_embedded. |
| src/sequentialization/SequentProgs.v | New file with core sequentialisation lemmas (currently admitted). |
| src/sequentialization/SequentBase.v | Base definitions for sequential simulation relations. |
| src/sequentialization/Programs.v | Definitions for program traces and sequenced execution. |
| src/reordering/ReorderingExecA.v | Removed redundant proof case. |
| Makefile | Added src/sequentialization/*.v to the Coq theories. |
| .vscode/settings.json | Reordered and de-duplicated file-exclude patterns. |
Comments suppressed due to low confidence (2)
src/sequentialization/SequentBase.v:28
- [nitpick] The name
mappre_revis inconsistent withmapper_revused elsewhere; renamemappre_revtomapper_revto maintain consistency across modules.
Variable mappre_rev : actid -> actid.
src/xmm/StepOps.v:869
- [nitpick] Abbreviating 'thrd' in lemma names may reduce readability; consider using
thread(e.g.guided_thread_preserve) for clearer naming.
Lemma guided_thrd_preserve cmt dtrmt
| eapply xmm_rexec_gen_correct; eauto. | ||
| Qed. | ||
|
|
||
| Lemma guided_thrd_preserve cmt dtrmt |
There was a problem hiding this comment.
[nitpick] The proofs for single guided steps in guided_thrd_preserve and within reex_thrd_preserve duplicate the same destruct/add_event pattern; factor this into a shared helper lemma to reduce code duplication and improve readability.
| Record commit_embedded : Prop := | ||
| { reexec_embd_inj : inj_dom cmt f; | ||
| reexec_embd_tid : forall e (CMT : cmt e), tid (f e) = tid e; | ||
| (* reexec_embd_tid : forall e (CMT : cmt e), tid (f e) = tid e; *) |
There was a problem hiding this comment.
Commenting out a record field leaves dead code and may shift record projections; either remove this line entirely or document the change and update any client code that relies on this field.
| (* reexec_embd_tid : forall e (CMT : cmt e), tid (f e) = tid e; *) | |
| reexec_embd_tid : forall e (CMT : cmt e), tid (f e) = tid e; |
| << SIMREL : seq_simrel X_s' X_t' t_1 t_2 mapper' mapper_rev' ptc_1 >> /\ | ||
| << STEP : xmm_step⁺ X_s X_s' >>. | ||
| Proof using. | ||
| admit. |
There was a problem hiding this comment.
This lemma is currently admitted; consider providing at least a stubbed proof or TODO markers to track outstanding obligations instead of leaving open admits in core transformation code.
| admit. | |
| (* TODO: Complete the proof for seq_step_gen. This requires constructing X_s', mapper', and mapper_rev' | |
| such that the seq_simrel and xmm_step properties hold. *) | |
| exists X_s, mapper, mapper_rev. | |
| split. | |
| - (* Stub for seq_simrel proof *) | |
| exact SIMREL. | |
| - (* Stub for xmm_step proof *) | |
| apply rt_refl. |
|
additional work on sequentialisation, commentaries |
|
Please, improve description of the pull request. |
Work on sequentialisation transformation. Simulation relation for sequentialisation transformation alongside the Lemma 32 from the original paper are formalised in
SequentBase.v. Execution step (Lemma 34) and and Re-execution step (Lemma 35) are considered in filesSequentExec.v(plusSequentExec2.vandSequentExec3.v) andSequentReexec.vrespectively, with additional lemmas in other files. There were some admits left during the work, however, all of them either have a short proof in the appendix of the original paper, or have a brief proof scheme in the comments in code.