Prosa Refactoring Effort

The purpose of this file is to keep track of which files still need to be ported to the new refactored Prosa (the ‘behavior’ model). Check off a file once you have verified that either

• all still-relevant definitions and lemmas have been ported to the new behavior model, or
• the file requires no porting or is no longer relevant.

Files in the util module are not being tracked as it is presumed that they will not require to be ported.

Behavioral Model

• ./model/time.v
• ./model/suspension.v ❗ — task parameter and validity constraints are still missing
• ./model/schedule/uni/workload.v
• ./model/schedule/uni/schedulability.v
• ./model/schedule/uni/sustainability.v ❗
• ./model/policy_tdma.v
• ./model/priority.v
• ./model/schedule/uni/schedule.v
• ./model/schedule/uni/end_time.v ⁉
• ./model/schedule/uni/schedule_of_task.v
• ./model/schedule/uni/response_time.v
• ./model/schedule/uni/service.v

Ideal L&L Model

• ./model/schedule/uni/basic/platform.v
• ./model/schedule/uni/basic/platform_tdma.v
• ./model/arrival/basic/arrival_bounds.v
• ./model/arrival/basic/task.v
• ./model/arrival/basic/arrival_sequence.v
• ./model/arrival/basic/job.v
• ./model/arrival/basic/task_arrival.v

Arrival Curves

• ./model/arrival/curves/bounds.v

Jitter

• ./model/arrival/jitter/arrival_bounds.v — nothing equivalent exists, but it's questionable whether we'll need this anymore
• ./model/arrival/jitter/arrival_sequence.v
• ./model/arrival/jitter/job.v ❗ — task parameter and validity constraints are still missing
• ./model/arrival/jitter/task_arrival.v
• ./model/schedule/uni/jitter/schedule.v
• ./model/schedule/uni/jitter/platform.v
• ./model/schedule/uni/jitter/valid_schedule.v

Self-Suspensions

• ./model/schedule/uni/susp/suspension_intervals.v ❗

• ./model/schedule/uni/susp/schedule.v

• ./model/schedule/uni/susp/last_execution.v ⁉

• ./model/schedule/uni/susp/build_suspension_table.v ⁉

• ./model/schedule/uni/susp/platform.v

• ./model/schedule/uni/susp/valid_schedule.v

Non-Preemptive Workloads

• ./model/schedule/uni/nonpreemptive/schedule.v
• ./model/schedule/uni/nonpreemptive/platform.v

Limited-Preemptive Workloads

• ./model/schedule/uni/limited/schedule.v
• ./model/schedule/uni/limited/platform/util.v
• ./model/schedule/uni/limited/platform/preemptive.v
• ./model/schedule/uni/limited/platform/limited.v
• ./model/schedule/uni/limited/platform/definitions.v
• ./model/schedule/uni/limited/platform/priority_inversion_is_bounded.v
• ./model/schedule/uni/limited/platform/nonpreemptive.v
• ./model/schedule/uni/limited/abstract_RTA/abstract_seq_rta.v
• ./model/schedule/uni/limited/abstract_RTA/definitions.v
• ./model/schedule/uni/limited/abstract_RTA/reduction_of_search_space.v
• ./model/schedule/uni/limited/abstract_RTA/sufficient_condition_for_lock_in_service.v
• ./model/schedule/uni/limited/abstract_RTA/abstract_rta.v
• ./model/schedule/uni/limited/fixed_priority/response_time_bound.v
• ./model/schedule/uni/limited/fixed_priority/nonpr_reg/response_time_bound.v
• ./model/schedule/uni/limited/fixed_priority/nonpr_reg/nonpreemptive/response_time_bound.v
• ./model/schedule/uni/limited/fixed_priority/nonpr_reg/fixed/response_time_bound.v
• ./model/schedule/uni/limited/fixed_priority/nonpr_reg/floating/response_time_bound.v
• ./model/schedule/uni/limited/fixed_priority/nonpr_reg/preemptive/response_time_bound.v
• ./model/schedule/uni/limited/rbf.v

Transformation

• ./model/schedule/uni/transformation/construction.v

Uniprocessor Analyses

Basic

• ./model/schedule/uni/basic/busy_interval.v
• ./analysis/uni/basic/workload_bound_fp.v
• ./analysis/uni/basic/tdma_wcrt_analysis.v
• ./analysis/uni/basic/tdma_rta_theory.v
• ./analysis/uni/basic/fp_rta_theory.v
• ./analysis/uni/basic/fp_rta_comp.v

Jitter

• ./model/schedule/uni/jitter/busy_interval.v
• ./analysis/uni/jitter/workload_bound_fp.v
• ./analysis/uni/jitter/fp_rta_theory.v
• ./analysis/uni/jitter/fp_rta_comp.v

Limited-Preemptive

• ./model/schedule/uni/limited/busy_interval.v

Curves

• ./analysis/uni/arrival_curves/workload_bound.v

Dynamic Self-Suspensions via Suspension-Oblivious Analysis

• ./analysis/uni/susp/dynamic/oblivious/reduction.v
• ./analysis/uni/susp/dynamic/oblivious/fp_rta.v

Dynamic Self-Suspensions via Jitter Analysis

• ./analysis/uni/susp/dynamic/jitter/taskset_rta.v
• ./analysis/uni/susp/dynamic/jitter/taskset_membership.v
• ./analysis/uni/susp/dynamic/jitter/jitter_schedule_service.v
• ./analysis/uni/susp/dynamic/jitter/jitter_schedule_properties.v
• ./analysis/uni/susp/dynamic/jitter/jitter_taskset_generation.v
• ./analysis/uni/susp/dynamic/jitter/jitter_schedule.v
• ./analysis/uni/susp/dynamic/jitter/rta_by_reduction.v

Sustainability

• ./analysis/uni/susp/sustainability/allcosts/reduction_properties.v
• ./analysis/uni/susp/sustainability/allcosts/reduction.v
• ./analysis/uni/susp/sustainability/allcosts/main_claim.v
• ./analysis/uni/susp/sustainability/singlecost/reduction_properties.v
• ./analysis/uni/susp/sustainability/singlecost/reduction.v

Multiprocessor Behavioral Models

• ./model/schedule/apa/platform.v
• ./model/schedule/apa/interference.v
• ./model/schedule/apa/constrained_deadlines.v
• ./model/schedule/apa/affinity.v
• ./model/schedule/apa/interference_edf.v
• ./model/schedule/partitioned/schedule.v
• ./model/schedule/partitioned/schedulability.v
• ./model/schedule/global/transformation/construction.v
• ./model/schedule/global/basic/schedule.v
• ./model/schedule/global/basic/platform.v
• ./model/schedule/global/basic/interference.v
• ./model/schedule/global/basic/constrained_deadlines.v
• ./model/schedule/global/basic/interference_edf.v
• ./model/schedule/global/response_time.v
• ./model/schedule/global/workload.v
• ./model/schedule/global/jitter/schedule.v
• ./model/schedule/global/jitter/platform.v
• ./model/schedule/global/jitter/interference.v
• ./model/schedule/global/jitter/constrained_deadlines.v
• ./model/schedule/global/jitter/job.v
• ./model/schedule/global/jitter/interference_edf.v
• ./model/schedule/global/schedulability.v

Multiprocessor Analyses

• ./analysis/apa/workload_bound.v
• ./analysis/apa/interference_bound_fp.v
• ./analysis/apa/bertogna_fp_theory.v
• ./analysis/apa/bertogna_edf_theory.v
• ./analysis/apa/interference_bound.v
• ./analysis/apa/interference_bound_edf.v
• ./analysis/apa/bertogna_edf_comp.v
• ./analysis/apa/bertogna_fp_comp.v
• ./analysis/global/parallel/workload_bound.v
• ./analysis/global/parallel/interference_bound_fp.v
• ./analysis/global/parallel/bertogna_fp_theory.v
• ./analysis/global/parallel/bertogna_edf_theory.v
• ./analysis/global/parallel/interference_bound.v
• ./analysis/global/parallel/interference_bound_edf.v
• ./analysis/global/parallel/bertogna_edf_comp.v
• ./analysis/global/parallel/bertogna_fp_comp.v
• ./analysis/global/basic/workload_bound.v
• ./analysis/global/basic/interference_bound_fp.v
• ./analysis/global/basic/bertogna_fp_theory.v
• ./analysis/global/basic/bertogna_edf_theory.v
• ./analysis/global/basic/interference_bound.v
• ./analysis/global/basic/interference_bound_edf.v
• ./analysis/global/basic/bertogna_edf_comp.v
• ./analysis/global/basic/bertogna_fp_comp.v
• ./analysis/global/jitter/workload_bound.v
• ./analysis/global/jitter/interference_bound_fp.v
• ./analysis/global/jitter/bertogna_fp_theory.v
• ./analysis/global/jitter/bertogna_edf_theory.v
• ./analysis/global/jitter/interference_bound.v
• ./analysis/global/jitter/interference_bound_edf.v
• ./analysis/global/jitter/bertogna_edf_comp.v
• ./analysis/global/jitter/bertogna_fp_comp.v

Implementations

• ./implementation/task.v
• ./implementation/uni/basic/schedule.v
• ./implementation/uni/basic/fp_rta_example.v
• ./implementation/uni/basic/schedule_tdma.v
• ./implementation/uni/basic/tdma_rta_example.v
• ./implementation/uni/basic/extraction_tdma.v
• ./implementation/uni/jitter/schedule.v
• ./implementation/uni/jitter/fp_rta_example.v
• ./implementation/uni/jitter/task.v
• ./implementation/uni/jitter/arrival_sequence.v
• ./implementation/uni/jitter/job.v
• ./implementation/uni/susp/dynamic/oblivious/fp_rta_example.v
• ./implementation/uni/susp/dynamic/task.v
• ./implementation/uni/susp/dynamic/arrival_sequence.v
• ./implementation/uni/susp/dynamic/job.v
• ./implementation/uni/susp/schedule.v
• ./implementation/apa/bertogna_edf_example.v
• ./implementation/apa/schedule.v
• ./implementation/apa/task.v
• ./implementation/apa/bertogna_fp_example.v
• ./implementation/apa/arrival_sequence.v
• ./implementation/apa/job.v
• ./implementation/arrival_sequence.v
• ./implementation/global/parallel/bertogna_edf_example.v
• ./implementation/global/parallel/bertogna_fp_example.v
• ./implementation/global/basic/bertogna_edf_example.v
• ./implementation/global/basic/schedule.v
• ./implementation/global/basic/bertogna_fp_example.v
• ./implementation/global/jitter/bertogna_edf_example.v
• ./implementation/global/jitter/schedule.v
• ./implementation/global/jitter/task.v
• ./implementation/global/jitter/bertogna_fp_example.v
• ./implementation/global/jitter/arrival_sequence.v
• ./implementation/global/jitter/job.v
• ./implementation/job.v