Add lemmas about [service_of_jobs] (!204) · Merge requests · RT-PROOFS / PROSA - Formally Proven Schedulability Analysis · GitLab

Snippets Groups Projects

Merged Sergey Bozhko requested to merge sbozhko/rt-proofs:new_service_lemmas into master 3 years ago

Apr 14, 2022
- add lemmas about [service_of_jobs] · e3567e95
  Sergey Bozhko authored 3 years ago and Björn Brandenburg committed 3 years ago
  
  This commit also removes one spurious dependency on ideal uni-processor. That is, previously file [model/service_of_jobs.v] imported [processor.ideal], which is wrong, since [model/service_of_jobs.v] assumes no specific model for processor.
  e3567e95
- introduce the notion of "total service of jobs" · e3757dbb
  Sergey Bozhko authored 3 years ago and Björn Brandenburg committed 3 years ago
  
  e3757dbb