Generalize ideal aRTA

Summary of the changes:

• Interference and Interfering workload are now type-classes

• Generalizes aRTA to "multi-stage" aRTA

• IBF supports arbitrary parameters (not just relative arrival time). IBF parametrised by the relative arrival time is not expressive enough to support restricted-supply analysis. It was generalized to support a larger class of parameters

• Rename file [run to completion] file into [lower bound on service]. The file was slightly generalized, now it derives a lower bound on any pre-defined amount of service.

• Generalize instantiations of interference and interfering workload. Now, the definitions do not directly destruct the processor state.

marked as a Work In Progress

changed the description

added 24 commits

• b4ea2977...33a48458 - 8 commits from branch RT-PROOFS:master
• 8efbfeed - Add setoid rewrite
• 3aa01f5e - Generalize ideal aRTA
• 06327f7b - All
• 482c1632 - Del from search
• bce4c17c - Del some lemmas about existence of busy interval
• 6ba86b98 - Close some proofs
• cf3c33cc - Update
• b6a4e162 - Update
• d15b7b4f - Split new readiness
• 9eb83bc8 - Update
• 4065a825 - Close one lemma
• a9c3b9b6 - Remove sequentiality from EDF
• 40a6bab8 - Delete sequentiality for FP
• 4bc50c69 - No admitted proofs
• e0195027 - Show that [sequential_readiness] is [nonclairvoyant_readiness]
• b10e67ee - Polish one file

Compare with previous version

added 14 commits

• 49b1ce79 - All
• c05aaf72 - Del from search
• c1d7c625 - Del some lemmas about existence of busy interval
• fc6087e6 - Close some proofs
• 0fccb7c5 - Update
• b48bdedc - Update
• 961324d2 - Split new readiness
• 7d8937a2 - Update
• 0d6d35a4 - Close one lemma
• cb2dfc6d - Remove sequentiality from EDF
• 0a16ad96 - Delete sequentiality for FP
• 12179cd7 - No admitted proofs
• 55ca68b8 - Show that [sequential_readiness] is [nonclairvoyant_readiness]
• d4ed2148 - Polish one file

Compare with previous version

added 7 commits

• 109324ac - 1 commit from branch RT-PROOFS:master
• d25c12b1 - optimize names for run-to-completion threshold functions
• 3842a214 - Add setoid rewrite
• 40695a49 - add notion of sequential readiness
• 4b99f492 - add lemmas to sum.v
• e4347eea - test
• 0dfd67dc - Restricted supply

Compare with previous version

added 1 commit

• bf5ce62e - Add new file

Compare with previous version

What's the state of the MR? Do you think this is going to converge into mergeable state in the foreseeable future? What's missing?

added 8 commits

• bf5ce62e...c14a8266 - 2 commits from branch RT-PROOFS:master
• 8002b3df - Add setoid rewrite
• 7aff0b19 - add notion of sequential readiness
• 6e450597 - add lemmas to sum.v
• 32353da2 - test
• e1c4bc5a - Restricted supply
• 8c1cc5d3 - Add new file

Compare with previous version

added 8 commits

• 8c1cc5d3...aed29c33 - 3 commits from branch RT-PROOFS:master
• 318436f2 - Add setoid rewrite
• 9f945c0c - add notion of sequential readiness
• 2e26b267 - all
• 6b12553e - Restricted supply
• ef1a6a61 - Dummy file

Compare with previous version

mentioned in issue #76 (closed)

added 17 commits

• d9c2963c - add notion [receives_service_at]
• beccc4ea - (WIP/del) restructure [service_of_jobs]
• e550a6fe - ddddd
• 419bae56 - change basic readiness to sequential readiness
• 478ce819 - hm
• a93c54c9 - Changewefwef
• 19a7ba65 - change this
• b0fb7e6d - I/W to TypeClass
• 0d260073 - Changewefwef
• 1c5cbdd6 - MOVE
• 1f56bdae - all
• c0c00db4 - Restricted supply
• 9fbf4855 - Dummy file
• aa1988ce - MOVE / DEL
• 61708a43 - MOVE
• 3e5778e2 - MOVE / DEL
• e095ba3c - move(?)

Compare with previous version

added 24 commits

• e095ba3c...271464a5 - 5 commits from branch RT-PROOFS:master
• 19b69dfa - Add setoid rewrite
• 60c2d31f - add notion of sequential readiness
• aa977cd7 - add notion [receives_service_at]
• c481fe5e - (WIP/del) restructure [service_of_jobs]
• 63c4fcd6 - ddddd
• 96fffcff - change basic readiness to sequential readiness
• a0d349d2 - hm
• 59f7d421 - Changewefwef
• 57f46cde - change this
• 91524fe6 - I/W to TypeClass
• 3732213c - Changewefwef
• 25000fb7 - MOVE
• 03396a49 - all
• 92cd1cb9 - Restricted supply
• dc08537e - Dummy file
• 121f4f8a - MOVE / DEL
• ac4658d6 - MOVE
• 88691b18 - MOVE / DEL
• 5a5fc5f2 - move(?)

Compare with previous version

added 21 commits

• 5a5fc5f2...18ec53fb - 3 commits from branch RT-PROOFS:master
• ca8e2e36 - add notion of sequential readiness
• 2ebb51bc - add notion [receives_service_at]
• b0351c53 - (WIP/del) restructure [service_of_jobs]
• 65f75b16 - ddddd
• 3ab39ada - change basic readiness to sequential readiness
• 0f0c8db9 - hm
• b83abbb7 - Changewefwef
• b995baf9 - change this
• 87b4c3ed - I/W to TypeClass
• 65347c97 - Changewefwef
• 5ff0dc91 - MOVE
• 4dafd9fd - all
• ddb31166 - Restricted supply
• e76fb23f - Dummy file
• eb6d3222 - MOVE / DEL
• 46c3b3a4 - MOVE
• a2fa9202 - MOVE / DEL
• 7d92d321 - move(?)

Compare with previous version

added 22 commits

• 7d92d321...9f99f33f - 7 commits from branch RT-PROOFS:master
• 913fb9b0 - add notion [receives_service_at]
• fcc76ef4 - (WIP/del) restructure [service_of_jobs]
• 08d56e81 - ddddd
• faace733 - hm
• 0d721b68 - I/W to TypeClass
• 23fbf361 - Changewefwef
• f91883ad - MOVE
• ace55725 - all
• db9e21ca - Restricted supply
• 70908b60 - Dummy file
• e96977e1 - MOVE / DEL
• 14682bd5 - MOVE
• 093271d5 - MOVE / DEL
• beda4e67 - move(?)
• afafacd0 - ??

Compare with previous version

added 12 commits

• dca8182f - (WIP/del) restructure [service_of_jobs]
• 883e3ac0 - hm
• 6771b5cc - I/W to TypeClass
• 3276585b - Changewefwef
• 2f4ca158 - all
• 4c581aa9 - Restricted supply
• ed6b82a9 - Dummy file
• d449fd1e - MOVE / DEL
• 63fe2c40 - MOVE
• 1116b0a5 - MOVE / DEL
• d79223e7 - move(?)
• 39419e0c - ??

Compare with previous version

added 8 commits

• 39419e0c...ac4fcc46 - 2 commits from branch RT-PROOFS:master
• d4170267 - aux things
• 57e3892a - generalize aRTA
• 6dd65b18 - restricted supply
• aa7ec21d - move / del
• d68647c3 - ffff
• 49b26b32 - add notion `receives_service_at`

Compare with previous version

added 7 commits

• ca830af5 - aux things
• 3d33163f - generalize aRTA
• 348dd228 - restricted supply
• 6f2342d0 - move / del
• 073c94f3 - ffff
• f444f96a - add notion `receives_service_at`
• 91f2a139 - some initial fixes

Compare with previous version

added 8 commits

• 1aca792a - aux things
• 86e4e6ec - priority inversion
• 6fc825a2 - generalize aRTA
• ad5400ce - restricted supply
• b1abc7ec - move / del
• 5aa35ca6 - ffff
• 08e7cdd3 - add notion `receives_service_at`
• d91e7019 - some initial fixes

Compare with previous version

added 10 commits

• d91e7019...bc38ff74 - 2 commits from branch RT-PROOFS:master
• e050eff4 - aux things
• 3f5857a7 - priority inversion
• 4845890a - generalize aRTA
• 36b52fa2 - restricted supply
• 1d829bb9 - ffff
• 82f29cd6 - add notion `receives_service_at`
• aceda2ce - to del
• b6cb8f46 - fix

Compare with previous version

added 196 commits

• b6cb8f46...56abdd37 - 188 commits from branch RT-PROOFS:master
• a337342c - add auxiliary lemmas about ideal schedule
• c5ef86ec - add lemma about [service_of_jobs_at]
• c9b5214c - generalize priority inversion definition
• a163372b - : add notion of service inversion
• 0936d9f9 - : add lemmas about task service
• 18ce6c6c - : add helper lemmas
• c40a4206 - : generalize aRTA
• 7c21d6ca - : restricted supply

Compare with previous version

added 14 commits

• 7c21d6ca...d852a1ce - 7 commits from branch RT-PROOFS:master
• b3356dea - : add notion of service inversion
• 6db2b5b0 - : add lemmas about task service
• 3c3baaba - : create merge hell for no reason
• 055d5635 - : add helper lemmas
• 11371817 - : del?
• 32dd60af - : generalize aRTA
• 4de30cff - : restricted supply

Compare with previous version

added 7 commits

• ac23fb57 - : clean up [abstract.definitions]
• d4f1dbde - : add notion of service inversion
• 635ede83 - : add lemmas about task service
• aef9c8fe - : create merge hell for no reason
• b3c87350 - : add helper lemmas
• fb32a85d - : generalize aRTA
• c0892cb8 - : restricted supply

Compare with previous version

added 7 commits

• f96f8c77 - : generalize aRTA
• 79244226 - : JLFP instantiation
• 0ddce660 - : add notion of service inversion
• 2b23f053 - : add lemmas about task service
• 35a3476b - : create merge conflict hell for no reason
• fd44e701 - : this probably can be removed
• 926c21fd - : restricted supply

Compare with previous version

added 8 commits

• b4bc4e22 - : squash
• d138848b - : remove ideal proc from jlfp-inst
• c8986fa7 - : JLFP instantiation
• bbdcc661 - : add notion of service inversion
• ff96dc77 - : add lemmas about task service
• 59d04e88 - : create merge conflict hell for no reason
• b61281a6 - : this probably can be removed
• e343e698 - : restricted supply

Compare with previous version

added 7 commits

• a504570c - : remove ideal proc from jlfp-inst
• 01d6ac69 - : JLFP instantiation
• bba329b8 - : add notion of service inversion
• e51950ef - : add lemmas about task service
• c6189868 - : create merge conflict hell for no reason
• 02ea96cc - : this probably can be removed
• 35db31db - : restricted supply

Compare with previous version

added 7 commits

• 774fcd79 - : update some old proofs
• 6e1e7cf6 - : JLFP instantiation
• b3df7762 - : add notion of service inversion
• 661dec07 - : add lemmas about task service
• da8c6817 - : create merge conflict hell for no reason
• 0da82798 - : this probably can be removed
• ff9e66e0 - : restricted supply

Compare with previous version

added 7 commits

• 1ebe68aa - : prove and move some stuff
• 8503bf62 - : JLFP instantiation
• b0990ffb - : add notion of service inversion
• 97509999 - : add lemmas about task service
• 1fe9e14a - : create merge conflict hell for no reason
• 845fa8e4 - : this probably can be removed
• 9b0340d8 - : restricted supply

Compare with previous version

added 7 commits

• 2da2d95d - : port a few more lemmas
• 7b6d503e - : JLFP instantiation
• 96e678f9 - : add notion of service inversion
• ae273552 - : add lemmas about task service
• 09f4872e - : create merge conflict hell for no reason
• 4205cae2 - : this probably can be removed
• dd6ba67d - : restricted supply

Compare with previous version

added 7 commits

• 8e6857a3 - : generalize ideal-JLFP instantiation
• f1a9066d - : JLFP instantiation
• cd74f5b6 - : add notion of service inversion
• 2769bf28 - : add lemmas about task service
• a2273b1b - : create merge conflict hell for no reason
• 02989f88 - : this probably can be removed
• 9f7adf51 - : restricted supply

Compare with previous version

added 7 commits

• 2bd6167e - : work on one lemma
• c7952296 - : JLFP instantiation
• 926b89fb - : add notion of service inversion
• 079fa3c8 - : add lemmas about task service
• d74376eb - : create merge conflict hell for no reason
• 87830809 - : this probably can be removed
• c7f0dc9a - : restricted supply

Compare with previous version

added 6 commits

• 4df06299 - : generalize aRTA
• e101631c - : add notion of service inversion
• 6da59a61 - : add lemmas about task service
• 065c8dd7 - : create merge conflict hell for no reason
• 9bc300c7 - : this probably can be removed
• 51f7461c - : restricted supply

Compare with previous version

added 6 commits

• c4182555 - close one proof
• e084baf9 - : add notion of service inversion
• a1398812 - : add lemmas about task service
• 000155fb - : create merge conflict hell for no reason
• bf953463 - : this probably can be removed
• 830d7794 - : restricted supply

Compare with previous version

added 7 commits

• 60680c6a - : close one proof
• 1bfe4f5d - : close a few more lemmas
• 9cd9b4d9 - : add notion of service inversion
• e57cb5fb - : add lemmas about task service
• beb0f181 - : create merge conflict hell for no reason
• d73a05d3 - : this probably can be removed
• 1a54beff - : restricted supply

Compare with previous version

added 6 commits

• 315a83f4 - : close a few more lemmas
• f0ebd787 - : add notion of service inversion
• 9845b942 - : add lemmas about task service
• b45ee0c4 - : create merge conflict hell for no reason
• 15f28529 - : this probably can be removed
• 31a861b4 - : restricted supply

Compare with previous version

added 6 commits

• 84309837 - : add lemma about equiv of busy prefix
• 849d1462 - : add notion of service inversion
• 9a89f570 - : add lemmas about task service
• 6fcab2bd - : create merge conflict hell for no reason
• fc65bdaa - : this probably can be removed
• 88cac166 - : restricted supply

Compare with previous version

added 6 commits

• edd05349 - : close a few more lemmas
• 278771ed - : add notion of service inversion
• ce150da8 - : add lemmas about task service
• a0ef0791 - : create merge conflict hell for no reason
• 93419201 - : this probably can be removed
• 47650693 - : restricted supply

Compare with previous version

added 6 commits

• 347fe0b6 - : close a few lemmas
• e0ddb81f - : add notion of service inversion
• 6ae8817a - : add lemmas about task service
• 9863d008 - : create merge conflict hell for no reason
• e4bebf68 - : this probably can be removed
• 8f8c32b9 - : restricted supply

Compare with previous version

added 7 commits

• 0bb7b0e3 - : add notion of service inversion
• 8d70f7ed - : close a few lemmas
• 8ef33277 - : some mediocre progress
• cf1f0054 - : add lemmas about task service
• 8a10efab - : create merge conflict hell for no reason
• 367c847b - : this probably can be removed
• 281f1021 - : restricted supply

Compare with previous version

added 5 commits

• 54388fbf - : some progress with rewriting a lemma
• c98b1f53 - : add lemmas about task service
• 20ac3592 - : create merge conflict hell for no reason
• c2356335 - : this probably can be removed
• d8bfd4f9 - : restricted supply

Compare with previous version

added 5 commits

• 141c13db - : close one lemma
• ec73b915 - : add lemmas about task service
• 1dfe05cf - : create merge conflict hell for no reason
• 5c61958c - : this probably can be removed
• 8a7566ad - : restricted supply

Compare with previous version

added 5 commits

• 5a731bf8 - : close a few more lemmas
• 4bbaad13 - : add lemmas about task service
• 3b5a17ff - : create merge conflict hell for no reason
• f442cec7 - : this probably can be removed
• fc7df258 - : restricted supply

Compare with previous version

added 3 commits

• 964086e7 - : generalize aRTA
• 30e128b9 - : add notion of service inversion
• 06c23625 - : add lemmas about task service

Compare with previous version

added 24 commits

• 06c23625...fcdb00b9 - 15 commits from branch RT-PROOFS:master
• 52f52a97 - improve tactics
• c998565c - add notion of service inversion
• 9ddc26ac - add lemmas about task service
• a51504f2 - add reflection for priority inversion
• 030b922d - generalize abstract RTA
• a91d9303 - : to merge
• 96d041a2 - : to merge
• 16f4a6d8 - : to merge
• 6b9de0f6 - : move these files to prev. commit

Compare with previous version

added 4 commits

• 9544d66c - generalize abstract RTA
• 1a3aa852 - : to merge
• f6e0d960 - : to merge
• 9b676ff3 - : move these files to prev. commit

Compare with previous version

added 5 commits

• 915fe4b6 - : introduce [job_workload_between]
• 81673d05 - generalize abstract RTA
• deccc33c - : merge
• c5f2fc7b - : merge
• 952598cb - : move these files to prev. commit

Compare with previous version

added 9 commits

• e2d2c381 - : add notion of service inversion
• 2a08ae6a - : add lemmas about task service
• 343d332e - : add reflection for priority inversion
• aab243a9 - : introduce [job_workload_between]
• 835b1582 - : generalize abstract RTA
• de0cb5b8 - : merge
• 2878ab64 - : merge
• 27e5789c - : merge
• 5dd3bf1b - : merge

Compare with previous version

added 5 commits

• fc9f55e8 - : add lemmas about TODO
• b6577397 - : generalize abstract RTA
• dc4611a5 - : merge
• a32a3a23 - : merge
• 023bb4ca - : merge

Compare with previous version

added 12 commits

• 572e7792 - minor improvements in tabulation
• 4ff9f929 - optimize imports
• e41bf5da - : add notion of service inversion
• 6cb2f2f1 - : add lemmas about task service
• f13d1287 - : add reflection for priority inversion
• 5c48f13c - : introduce [job_workload_between]
• 374170a2 - : add lemmas about job relations
• 68fb6b5b - : generalize abstract RTA
• 78a5e319 - : merge
• 42c3ef5b - : merge
• 81c01478 - : merge
• 32e07c0f - : merge

Compare with previous version