upenn-acg / verified-tsan Goto Github PK

In instrument_sim_safe, we assumed that the original program and the instrumented program has the same memory m before making the step(s); this causes a problem when proving instrument_correct, because the initial memory for the instrumented program is m0, whereas that of the original program should be [] (if we assume the original program also has its initial memory being m0, then the hypothesis Hroot may not be satisfied). @mansky1 How about we change the hypothesis of instrument_sim_safe such that assume something like mem_sim' m1 m2 /\ consistent m1, where m1,m2 are the initial memory of the instrumented and original program, respectively?

The desired lemma has been stated(but not yet proved) here.

A lemma stating sth. like "initialized m x -> can_write m x" is needed when proving consistent_mem_vals & consistent_mem_vals'.

In order to prove the clause about memory consistency, I wrote down a lemma here. @mansky1 William, would you mind taking a look at it to make sure it's provable?

In case we forget about them after the reordering lemmas are finished.

There's a gap left in the current instrument_correct_race, which exec_fail_iexec failed to bridge. We need an extended version of exec_fail_iexec to resolve this.

needed at several places in instrument_correct & instrument_correct_race:
admit1;
admit2;
admit3

This issue arose in the proof of legal_tids_steps, and instrument_sim_safe': after doing an induction on Hsteps and Hstep, the base case looks unprovable. @mansky1