Port non-seq aRTA

Mostly it is just a copy-paste of the old Abstract RTA.

However, I add a new section FixpointIsNoLessThanArrival in file abstract_rta.v; so comments are very welcome.

PDF-file for convenience: abstract.core.abstract_rta.pdf

changed the description

added 1 commit

• f7c9adeb - Comment fix

Compare with previous version

added 1 commit

• eb1a8465 - Delete commented part

Compare with previous version

Overall, the MR looks good to me. In particular, the new step-wise proof in FixpointIsNoLessThanArrival is a nice improvement, thank you for that.

There are a couple of cosmetic things; not blocking issues but it would be nice to have fixed before the merge. Please see my inline comments.

One perhaps slightly more significant aspect is that job_lock_in_service should be a type class, to be consistent with all other job parameters. Do you agree?

added 1 commit

• d397aacd - Fix comment in aRTA defs.

Compare with previous version

added 1 commit

• 6a4d1a5b - Rename proper ~> valid

Compare with previous version

added 15 commits

• 3ac09ade - Add new generic type of parameter
• 1d9a0c30 - Update
• 005f603f - Add platform
• c4150cfe - Move files
• df2e7582 - Delete work-conserving def
• 9832259c - Delete prio.pol.
• 7464b8c5 - Update
• 7e27391a - Done with job_rtct proofs
• 10e4cd08 - Done with proofs
• bac8ab00 - Del sched. file
• 89cb2ce8 - Del things in preemption model
• c2055421 - Rename
• dd2c2bcb - Rename: lock-in ~> run-to-compl
• a79308bc - Fix comments in rtct
• 70eec79f - Rename some files

Compare with previous version

added 1 commit

• 779fed64 - Del. useless files

Compare with previous version

resolved all threads