Reorganize and clean up restructuring.module
This patch series completely re-shuffles how the rt.restructuring.model module is organized. I believe this to be much more logically meaningful and easier to work with in the future.
There are now the following sub-modules:
- model.aggregate: functions on sets of jobs (unchanged)
- model.arrival: arrival models for tasks (unchanged), to be extended with periodic, etc. ...
- model.preemption: the new preemption model for jobs (no mention of tasks)
- model.priority: FP/JFLP/JLDP policies, to be extended with FIFO, RM, DM, ...
- model.processor: processor models and platform properties (unchanged)
- model.readiness: various way to define
job_ready(unchanged), to be extended with self-suspensions... - model.schedule: definitions related to schedules, including priority-driven schedules
- model.task: everything about the task abstraction (except for arrivals, see above)
- model.task.preemption: the new preemption model for tasks
I recommend looking through it here: http://prosa.mpi-sws.org/branches/model-reorg/pretty/tree.html (scroll to the bottom).
@mlesourd @sophie @sbozhko: Please comment if anything sticks out. This organization is of course not set in stone; we can improve it later. So unless there are major concerns, I'd rather go ahead soon and worry about making it perfect in future revisions, as I think it's much better than what we've had so far and it blocks further clean-up work.
Note 1: the comments still need to be cleaned-up and improved; this is something for next week. (Help of course always welcome.)
Note 2: the analysis module will similarly have to be reorganized; this is pending and will be possible only after Sergey is done with the Require cleanup in analysis.
Merge request reports
Activity
mentioned in merge request !67 (merged)
mentioned in issue #37 (closed)
added 1 commit
- 3b486cb7 - update guidelines to state `Require Import|Export` rules
added 1 commit
- 63719701 - update guidelines to state `Require Import|Export` rules
added 39 commits
-
63719701...2e9c8416 - 11 commits from branch
require-removal - a258c252 - model reorg: move priorities definition to own folder
- 73653440 - model reorg: move EDF priority definition to model.priority
- ba758466 - model reorg: have only one notion of priority-driven schedules
- 4a80f261 - model reorg: move TDMA facts to analysis
- 393d2007 - model reorg: move preemption-time notion to model.schedule
- 9933d50d - model reorg: job.v is an analysis def; job_deadline a task property
- 65f28df9 - fix EDF priority definition to not depend on task abstraction
- eca90fdf - model reorg: 'sequential tasks' is a task property
- 42e6a42b - model reorg: move task concept to model.task.concept
- 9c7b4f30 - model reorg: move task preemption parameters to model.task.preemption
- 25754fea - model reorg: move task preemption models to model.task.preemption
- 572c699b - model reorg: move preemption.valid_schedule -> schedule.limited_preemptive
- 4e9768b1 - model reorg: task.sequential -> task.sequentiality
- 540acffd - model reorg: fold RTCT validity into task.preemption.parameters
- 7b64c4b0 - model reorg: fold RTCT instances into task.preemption.*
- f96feefc - model reorg: get rid of purely re-export models
- ba086071 - preemption_time.v should not depend on task concept
- 7b38326f - split job and tasks aspects in preemption.valid_model
- 4d5c9497 - model reorg: merge job_preemptable def and validity
- 1306c75c - model reorg: flatten model.preemption
- 12b573c3 - remove task dependency in job limited-preemptive preemption model
- 0bc2ea0b - remove unneeded Require in model.task.preemption.parameters
- 390228e8 - remove unneeded 'Require' statement in analysis spec
- ba8dc43b - Don't Export modules that introduce new Instances
- d14a37c0 - Improve comments in analysis
- 0089c2ce - Update README
- 1b7dd375 - remove unnecessary Require statements in model.task.preemption
- ddcd2790 - update guidelines to state `Require Import|Export` rules
Toggle commit list-
63719701...2e9c8416 - 11 commits from branch
