GitLab

We use simpler, more pessimistic interference bounds to
prove that Bertogna and Cirinei's RTA works for parallel jobs.

- Implemented concrete job and tasks.
- Added a periodic arrival sequence.
- Created examples of applying a schedulability
  test to small task sets and concluding that
  no task misses a deadline.

- Now we have two definitions of work conserving, a simple version
  and another one based on count, along with a proof of equivalence.

- Implemented a concrete scheduler (basic and jitter)

- Removed unnecessary assumption in RTA about task precedence/no intra-task parallelism.
- Scheduler models and analyses are organized in separate modules/folders.
- Added RTA for FP and EDF for schedulers with release jitter.
- The scheduling invariants were split into more fine-grained assumptions:
  (a) scheduler is work-conserving
  (b) scheduler enforces FP/JLDP priority X
- New helper lemmas about counting, and sorted/uniq lists
- Inclusion of tactics feed and feed_n (see documentation).
- Added a Makefile generator

Should allow jobs that arrive before the interval

Obviously incomplete, but a start.

An up-to-date version can always be generated with 'make html'.

First housekeeping steps...