Reorganize and clean up restructuring.module (!68) · Merge requests · RT-PROOFS / PROSA - Formally Proven Schedulability Analysis

Merged Björn Brandenburg requested to merge model-reorg into require-removal 5 years ago

Dec 03, 2019
- update guidelines to state `Require Import|Export` rules · ddcd2790
  Björn Brandenburg authored 5 years ago
  
  While at it, clean up some Markdown rendering issues on Gitlab.
  ddcd2790
- remove unnecessary Require statements in model.task.preemption · 1b7dd375
  Björn Brandenburg authored 5 years ago
  
  1b7dd375
- Update README · 0089c2ce
  Sergey Bozhko authored 5 years ago and Björn Brandenburg committed 5 years ago
  
  0089c2ce
- Improve comments in analysis · d14a37c0
  Sergey Bozhko authored 5 years ago and Björn Brandenburg committed 5 years ago
  
  d14a37c0
- Don't Export modules that introduce new Instances · ba8dc43b
  Sergey Bozhko authored 5 years ago and Björn Brandenburg committed 5 years ago
  
  ba8dc43b
- remove unneeded 'Require' statement in analysis spec · 390228e8
  Sergey Bozhko authored 5 years ago and Björn Brandenburg committed 5 years ago
  
  390228e8
- remove unneeded Require in model.task.preemption.parameters · 0bc2ea0b
  Björn Brandenburg authored 5 years ago
  
  0bc2ea0b
- remove task dependency in job limited-preemptive preemption model · 12b573c3
  Björn Brandenburg authored 5 years ago
  
  Job-level definitions should not depend on task-related modules.
  12b573c3
- model reorg: flatten model.preemption · 1306c75c
  Björn Brandenburg authored 5 years ago
  
  1306c75c
- model reorg: merge job_preemptable def and validity · 4d5c9497
  Björn Brandenburg authored 5 years ago
  
  4d5c9497
- split job and tasks aspects in preemption.valid_model · 7b38326f
  Björn Brandenburg authored 5 years ago
  
  The notion of a valid preemption model for *jobs* should not depend on any task abstraction. Split the two notions.
  7b38326f
- preemption_time.v should not depend on task concept · ba086071
  Björn Brandenburg authored 5 years ago
  
  This is a purely accidental dependency; purge it.
  ba086071
- model reorg: get rid of purely re-export models · f96feefc
  Björn Brandenburg authored 5 years ago
  
  With proper re-exports everywhere, this is no longer necessary.
  f96feefc
- model reorg: fold RTCT instances into task.preemption.* · 7b64c4b0
  Björn Brandenburg authored 5 years ago
  
  The two concepts are tightly coupled and it does not make sense to mix and match them. Therefore, it's cleaner and easier to understand if both aspects of the preemption model are instantiated in the same module next to each other.
  7b64c4b0
- model reorg: fold RTCT validity into task.preemption.parameters · 540acffd
  Björn Brandenburg authored 5 years ago
  
  No need to keep the two separate as they are tightly coupled anyway, and the joint file doesn't become too long.
  540acffd
- model reorg: task.sequential -> task.sequentiality · 4e9768b1
  Björn Brandenburg authored 5 years ago
  
  The property is a noun: a model of task sequentiality.
  4e9768b1
- model reorg: move preemption.valid_schedule -> schedule.limited_preemptive · 572c699b
  Björn Brandenburg authored 5 years ago
  
  All "kinds of schedules" and associated validity conditions are being collected in model.schedule.
  572c699b
- model reorg: move task preemption models to model.task.preemption · 25754fea
  Björn Brandenburg authored 5 years ago
  
  25754fea
- model reorg: move task preemption parameters to model.task.preemption · 9c7b4f30
  Björn Brandenburg authored 5 years ago
  
  9c7b4f30
- model reorg: move task concept to model.task.concept · 42e6a42b
  Björn Brandenburg authored 5 years ago
  
  42e6a42b
- model reorg: 'sequential tasks' is a task property · eca90fdf
  Björn Brandenburg authored 5 years ago
  
  eca90fdf
- fix EDF priority definition to not depend on task abstraction · 65f28df9
  Björn Brandenburg authored 5 years ago
  
  EDF is defined in terms of jobs, whether or not those jobs stem from tasks. Make sure our definition is general enough to capture the possibility of a set of jobs without associated tasks scheduled by EDF.
  65f28df9
- model reorg: job.v is an analysis def; job_deadline a task property · 9933d50d
  Björn Brandenburg authored 5 years ago
  
  9933d50d
- model reorg: move preemption-time notion to model.schedule · 393d2007
  Björn Brandenburg authored 5 years ago
  
  393d2007
- model reorg: move TDMA facts to analysis · 4a80f261
  Björn Brandenburg authored 5 years ago
  
  4a80f261
- model reorg: have only one notion of priority-driven schedules · ba758466
  Björn Brandenburg authored 5 years ago
  
  The Prosa notion of priority-driven scheduling depends on the preemption model. That is ok; any theory that doesn't want to deal with non-preemptive sections can simply Require Export the fully preemptive model and be done with it.
  ba758466
- model reorg: move EDF priority definition to model.priority · 73653440
  Björn Brandenburg authored 5 years ago
  
  73653440
- model reorg: move priorities definition to own folder · a258c252
  Björn Brandenburg authored 5 years ago
  
  a258c252

Reorganize and clean up restructuring.module

Merge request reports

Activity