Added edf_wc.v

added 1 commit

• a68dff1f - Add EDF_WC theorem

Compare with previous version

Very good, glad to see you got started without running into any issues.

Have a look at the proof of the EDF_optimality theorem. The key part after some setup is the following:

    set sched' := edf_transform sched.
    ∃ sched'. split; last split.
    - by apply edf_schedule_is_valid.
    - by apply edf_schedule_meets_all_deadlines_wrt_arrivals.
    - by apply edf_transform_ensures_edf.

Next steps:

1. There’s one theorem for each high-level property (validity, meeting of deadlines, being an EDF schedule) which are just applied to complete each branch of the proof. To prove your theorem, you can reuse all of these results. Please go ahead and do this, i.e., replace the Admitted. with a mostly complete proof, admitting only individual missing branches.

2. The key top-level property still missing is of course the fact that edf_transform sched maintains work conservation. Let’s call this theorem edf_transform_maintains_work_conservation (we prefer a verbose naming scheme in Prosa). Please state this theorem (with an admitted proof) and then complete the proof of your optimality + work-conservation theorem.

I’ve left some comments in the diff. Please mark the threads as “resolved” when you are done addressing the issues (or reply in the thread to ask a question if something doesn’t make sense).

resolved all threads

added 1 commit

• 0eeb6a15 - Finished edf_wc_opt theorem

Compare with previous version

You are off to a good start. Now the real work starts: proving edf_transform_maintains_work_conservation requires diving into the "guts" of the EDF transformation. You will need to establish the preservation of work-conservation at two layers:

1. If you unfold edf_transform, you'll find edf_transform_prefix. You'll need to establish the fact for this layer. For inspiration, have a look at the section EDFPrefixFacts in prosa.analysis.transform.edf_trans.
2. One layer below, you'll need to use prefix_map_property_invariance to get at make_edf_at. This is the heart of the EDF transformation and its logic is the reason why work-conservation is maintained.
3. Specifically, make_edf_at proceeds by swapping allocations in the given schedule, and uses the predicate relevant_pstate to find candidates for swapping. To show work-conservation, you'll need to exploit that
   • (a) make_edf_at only swaps non-idle instants, and that
   • (b) relevant_pstate also skips idle allocations, so make_edf_at doesn't affect where in the schedule idle times occur.

Doing all of this one go is probably too much. So I would suggest to first focus on

• understanding the big picture (familiarize yourself with all definitions and get a good intuition for how the make_edf_at swap works),
• getting all required "scaffolding" (e.g., section setup) in place, and
• attacking the top layer (prove edf_transform_maintains_work_conservation by means of a an admitted claim about edf_transform_prefix).

Before moving on to the other proofs, please touch base with me again.

resolved all threads

Just to make sure we don't wait on each other, please leave a comment here when you'd like me to give feedback on the next iteration.

added 1 commit

• e9108b35 - Proved edf_transform_maintains_wc

Compare with previous version

added 1 commit

• 97244831 - Added exists_extensionality

Compare with previous version

I'm done with the top layer lemma: edf_transform_maintains_work_conservation. I had to add the exists_extensionality file (which I guess might be helpful for other proofs so I put it in util) because I needed the lemma in the proof. For some reason, this lemma isn't in Coq's logic library nor is it a tactic in ssreflect even though its forall counterpart is there.

Should I get started with the next layer (proving edf_transform_prefix_maintains_work_conservation)?

added 1 commit

• 87a75cbd - Finished edf work conservation proof

Compare with previous version

I think I'm done with the proof. I had to add a lemma in analysis/transform/prefix.v as well. I briefly explained why this lemma is needed in the file. Please let me know if something needs to change/to be added.

Looking forward to working on the next proof :)

Awesome, good job! I'll try to catch up with you soon and look at the proof in detail. For context, I'm currently working with some colleagues towards a paper deadline, so I have very limited advising cycles.