Switch basic readiness to sequential readiness in [results] folder

This MR fixes problems that the basic readiness model causes to implementations.
Namely, consider the fixed-priority scheduling with basic readiness model. Note that neither fixed-priority nor basic readiness imply the order in which two jobs of the same task should execute. Which means that the generic priority-driven implementation of a scheduler "pick a pending job with the highest priority that is ready and execute it" lacks the essential determinism regarding which job of a task to execute first.
Sequential readiness resolves this issue by stating that only the first pending job of a task is ready.

Note that this MR depends in MRs !115 (merged), !129 (merged), and !132 (closed)

changed title from WIP: Switch readiness to WIP: Switch basic readiness to sequential readiness in [results] folder

changed the description

Maybe I can split this MR even further:
(1) the first commit (the readiness switch) and (2) the rest (clean up + separation for the notion of priority inversion)

CC: @mmaida @bbb

changed the description

assigned to @bbb

requested review from @mmaida

added 4 commits

• 193ca6df - clean up [service_of_jobs]
• 25b63fd2 - (WIP) add lemmas about [task_scheduled_at]
• 9eec8114 - (WIP) clean up notion of priority inversion
• 3e18c268 - (WIP) switch from basic readiness to sequential readiness

Compare with previous version

added 5 commits

• 65320669 - clean up [service] and [service_of_jobs]
• 522a93f1 - add lemmas about [task_scheduled_at]
• 9d5f1fb9 - (WIP) split pi and pi for ideal uni-processor
• 3070c9b6 - (WIP) switch from basic readiness to sequential readiness
• eb4aeb60 - fix

Compare with previous version

added 4 commits

• 7ea279e0 - del
• 128f31bf - eded
• 846f62bb - (WIP) switch from basic readiness to sequential readiness
• 5c5a8c0b - fix

Compare with previous version

added 3 commits

• bb7d2ec9 - clean up [service] and [service_of_jobs]
• 594edecb - add lemmas about [task_scheduled_at]
• c5cf68cb - (WIP) switch from basic readiness to sequential readiness

Compare with previous version

added 14 commits

• c5cf68cb...18ec53fb - 8 commits from branch RT-PROOFS:master
• 62155c47 - add notion of sequential and work bearing readiness
• 43721c0c - add notion [receives_service_at]
• 771f0f51 - clean up [service] and [service_of_jobs]
• 48fcd741 - add lemmas about [task_scheduled_at]
• 9285f733 - [WIP] switch from basic readiness to sequential readiness
• 30758998 - [WIP] some progress

Compare with previous version

added 12 commits

• 30758998...9f99f33f - 7 commits from branch RT-PROOFS:master
• bd4f0ab3 - add notion [receives_service_at]
• c9eeb71f - clean up [service] and [service_of_jobs]
• 74228736 - add lemmas about [task_scheduled_at]
• d07f98bd - [WIP] switch from basic readiness to sequential readiness
• ef4808e5 - [WIP] some progress

Compare with previous version

added 1 commit

• 629c99f1 - [WIP] a bit more progress

Compare with previous version

added 1 commit

• a11bcb0b - Closed all proofs, fixed all errors

Compare with previous version

added 1 commit

• b7cb5cd7 - Clean up the rest

Compare with previous version

marked this merge request as ready

added 10 commits

• 247244f7 - 1 commit from branch RT-PROOFS:master
• 623cc535 - add notion [receives_service_at]
• 9631d0d2 - clean up [service] and [service_of_jobs]
• 15d6147d - add lemmas about [task_scheduled_at]
• 69948b4a - [WIP] switch from basic readiness to sequential readiness
• 986810e6 - [WIP] some progress
• 8d09636c - [WIP] a bit more progress
• ab193202 - Closed all proofs, fixed all errors
• ca11d16d - Clean up the rest
• 49a10e4b - small fix

Compare with previous version