Skip to content

GitLab

R
rt-proofs
Commit 3b689961 authored by Björn Brandenburg's avatar Björn Brandenburg
Browse files
Options

enable proof-length checking during CI

parent 40436103
Hide whitespace changes
Inline Side-by-side
Showing with 320 additions and 0 deletions
.gitlab-ci.yml
View file @ 3b689961
...@@ -70,3 +70,9 @@ doc: ...@@ -70,3 +70,9 @@ doc:
- "with-proofs/" - "with-proofs/"
- "without-proofs/" - "without-proofs/"
expire_in: 1 week expire_in: 1 week
proof-length:
stage: process
image: python:3-alpine
script:
- scripts/proofloc.py --check --long-proofs scripts/known-long-proofs.json `find . -iname *.v`
scripts/known-long-proofs.json 0 → 100644
View file @ 3b689961
{
"manual_exceptions": {
},
"legacy_proofs": {
"./analysis/apa/bertogna_edf_comp.v": {
"bertogna_edf_comp_f_increases": 53,
"bertogna_edf_comp_iteration_preserves_order": 159,
"bertogna_edf_comp_rt_grows_too_much": 99,
"edf_claimed_bounds_finds_fixed_point_of_list": 76
},
"./analysis/apa/bertogna_edf_theory.v": {
"bertogna_cirinei_response_time_bound_edf": 49,
"bertogna_edf_all_cpus_in_affinity_busy": 52,
"bertogna_edf_all_cpus_in_subaffinity_busy": 51,
"bertogna_edf_alpha'_is_full": 106,
"bertogna_edf_interference_by_different_tasks": 43,
"bertogna_edf_interference_in_non_full_processors": 133,
"bertogna_edf_sum_exceeds_total_interference": 43
},
"./analysis/apa/bertogna_fp_comp.v": {
"fp_analysis_yields_response_time_bounds": 107
},
"./analysis/apa/bertogna_fp_theory.v": {
"bertogna_cirinei_response_time_bound_fp": 47,
"bertogna_fp_all_cpus_in_affinity_busy": 54,
"bertogna_fp_all_cpus_in_subaffinity_busy": 53,
"bertogna_fp_alpha'_is_full": 143,
"bertogna_fp_interference_by_different_tasks": 42,
"bertogna_fp_interference_in_non_full_processors": 149,
"bertogna_fp_sum_exceeds_total_interference": 42,
"bertogna_fp_workload_bounds_interference": 44
},
"./analysis/apa/interference_bound_edf.v": {
"interference_bound_edf_holds_for_single_job_that_completes_on_time": 86,
"interference_bound_edf_many_periods_in_between": 40
},
"./analysis/apa/workload_bound.v": {
"W_monotonic": 51,
"workload_bound_service_of_first_and_last_jobs": 45,
"workload_bounded_by_W": 48
},
"./analysis/global/basic/bertogna_edf_comp.v": {
"bertogna_edf_comp_f_increases": 53,
"bertogna_edf_comp_iteration_preserves_order": 160,
"bertogna_edf_comp_rt_grows_too_much": 100,
"edf_claimed_bounds_finds_fixed_point_of_list": 76
},
"./analysis/global/basic/bertogna_edf_theory.v": {
"bertogna_cirinei_response_time_bound_edf": 50,
"bertogna_edf_interference_by_different_tasks": 43,
"bertogna_edf_interference_in_non_full_processors": 129
},
"./analysis/global/basic/bertogna_fp_comp.v": {
"fp_analysis_yields_response_time_bounds": 105
},
"./analysis/global/basic/bertogna_fp_theory.v": {
"bertogna_cirinei_response_time_bound_fp": 48,
"bertogna_fp_interference_by_different_tasks": 42,
"bertogna_fp_interference_in_non_full_processors": 164,
"bertogna_fp_workload_bounds_interference": 45
},
"./analysis/global/basic/interference_bound_edf.v": {
"interference_bound_edf_holds_for_single_job_that_completes_on_time": 92,
"interference_bound_edf_many_periods_in_between": 40
},
"./analysis/global/basic/workload_bound.v": {
"W_monotonic": 51,
"workload_bound_service_of_first_and_last_jobs": 46,
"workload_bounded_by_W": 48
},
"./analysis/global/jitter/bertogna_edf_comp.v": {
"bertogna_edf_comp_f_increases": 53,
"bertogna_edf_comp_iteration_preserves_order": 160,
"bertogna_edf_comp_rt_grows_too_much": 100,
"edf_claimed_bounds_finds_fixed_point_of_list": 77
},
"./analysis/global/jitter/bertogna_edf_theory.v": {
"bertogna_cirinei_response_time_bound_edf": 60,
"bertogna_edf_interference_by_different_tasks": 63,
"bertogna_edf_interference_in_non_full_processors": 125
},
"./analysis/global/jitter/bertogna_fp_comp.v": {
"fp_analysis_yields_response_time_bounds": 120
},
"./analysis/global/jitter/bertogna_fp_theory.v": {
"bertogna_cirinei_response_time_bound_fp": 49,
"bertogna_fp_all_cpus_are_busy": 40,
"bertogna_fp_interference_by_different_tasks": 54,
"bertogna_fp_interference_in_non_full_processors": 173,
"bertogna_fp_workload_bounds_interference": 46
},
"./analysis/global/jitter/interference_bound_edf.v": {
"interference_bound_edf_holds_for_single_job_that_completes_on_time": 123,
"interference_bound_edf_holds_for_single_job_with_small_slack": 55,
"interference_bound_edf_j_fst_completed_on_time": 46,
"interference_bound_edf_many_periods_in_between": 49
},
"./analysis/global/jitter/workload_bound.v": {
"W_monotonic": 51,
"workload_bound_many_periods_in_between": 41,
"workload_bound_n_k_covers_middle_jobs": 40,
"workload_bound_service_of_first_and_last_jobs": 50,
"workload_bounded_by_W": 48
},
"./analysis/global/parallel/bertogna_edf_comp.v": {
"bertogna_edf_comp_f_increases": 53,
"bertogna_edf_comp_iteration_preserves_order": 159,
"bertogna_edf_comp_rt_grows_too_much": 96,
"edf_claimed_bounds_finds_fixed_point_of_list": 76
},
"./analysis/global/parallel/bertogna_edf_theory.v": {
"bertogna_cirinei_response_time_bound_edf": 49,
"bertogna_edf_interference_on_all_cpus": 75
},
"./analysis/global/parallel/bertogna_fp_comp.v": {
"fp_analysis_yields_response_time_bounds": 98
},
"./analysis/global/parallel/bertogna_fp_theory.v": {
"bertogna_cirinei_response_time_bound_fp": 41,
"bertogna_fp_all_cpus_are_busy": 78
},
"./analysis/global/parallel/interference_bound_edf.v": {
"interference_bound_edf_many_periods_in_between": 40,
"interference_bound_edf_n_k_covers_all_jobs": 45
},
"./analysis/uni/arrival_curves/workload_bound.v": {
"total_workload_le_total_rbf": 45,
"total_workload_le_total_rbf'": 41,
"total_workload_le_total_rbf''": 41
},
"./analysis/uni/basic/tdma_wcrt_analysis.v": {
"formula_not_sched_St": 45,
"formula_sched_St": 100,
"response_time_le_WCRT": 52
},
"./analysis/uni/susp/dynamic/jitter/jitter_schedule_properties.v": {
"sched_jitter_does_not_pick_j": 50,
"sched_jitter_respects_policy": 77
},
"./analysis/uni/susp/dynamic/jitter/jitter_schedule_service.v": {
"jitter_reduction_inductive_step_case2": 96,
"jitter_reduction_less_job_service_before_interval_case5": 44,
"jitter_reduction_service_jitter": 51
},
"./analysis/uni/susp/dynamic/jitter/taskset_rta.v": {
"valid_response_time_bound_of_tsk_i": 52
},
"./analysis/uni/susp/dynamic/oblivious/reduction.v": {
"sched_new_completed_jobs_dont_execute": 42
},
"./analysis/uni/susp/sustainability/allcosts/main_claim.v": {
"policy_is_weakly_sustainable": 63
},
"./analysis/uni/susp/sustainability/allcosts/reduction_properties.v": {
"executes_before_suspension_in_sched_new": 42,
"sched_new_has_shorter_total_suspension": 43,
"sched_new_respects_policy": 77,
"sched_new_work_conserving": 63,
"suspended_in_sched_new_no_service_since_execution": 46,
"suspended_in_sched_new_suspension_starts_no_earlier": 56
},
"./analysis/uni/susp/sustainability/singlecost/reduction_properties.v": {
"sched_susp_highercost_depends_only_on_prefix": 56,
"sched_susp_highercost_same_schedule": 81
},
"./implementation/apa/bertogna_fp_example.v": {
"schedulability_test_succeeds": 87
},
"./implementation/apa/schedule.v": {
"scheduler_has_no_duplicate_jobs": 55,
"scheduler_mapping_is_work_conserving": 46,
"scheduler_priority": 113
},
"./implementation/global/basic/bertogna_fp_example.v": {
"schedulability_test_succeeds": 40
},
"./implementation/global/jitter/bertogna_fp_example.v": {
"schedulability_test_succeeds": 41
},
"./implementation/global/parallel/bertogna_fp_example.v": {
"schedulability_test_succeeds": 59
},
"./implementation/uni/basic/fp_rta_example.v": {
"RTA_yields_these_bounds": 45
},
"./implementation/uni/basic/schedule_tdma.v": {
"respects_FIFO": 45
},
"./implementation/uni/basic/tdma_rta_example.v": {
"respects_TDMA_policy": 43
},
"./implementation/uni/jitter/fp_rta_example.v": {
"RTA_yields_these_bounds": 52
},
"./implementation/uni/susp/dynamic/oblivious/fp_rta_example.v": {
"RTA_yields_these_bounds": 51
},
"./implementation/uni/susp/schedule.v": {
"scheduler_depends_only_on_prefix": 52
},
"./model/schedule/global/basic/constrained_deadlines.v": {
"platform_cpus_busy_with_interfering_tasks": 65,
"platform_fp_cpus_busy_with_interfering_tasks": 82
},
"./model/schedule/global/basic/platform.v": {
"work_conserving_eq_work_conserving_count": 67
},
"./model/schedule/global/jitter/constrained_deadlines.v": {
"platform_cpus_busy_with_interfering_tasks": 65,
"platform_fp_cpus_busy_with_interfering_tasks": 85
},
"./model/schedule/global/jitter/platform.v": {
"work_conserving_eq_work_conserving_count": 68
},
"./model/schedule/uni/jitter/busy_interval.v": {
"busy_interval_is_bounded": 59,
"exists_busy_interval_prefix": 68,
"not_quiet_implies_exists_scheduled_hp_job": 46
},
"./model/schedule/uni/limited/abstract_RTA/abstract_rta.v": {
"in": 115
},
"./model/schedule/uni/limited/abstract_RTA/abstract_seq_rta.v": {
"bound_for_cumulative_job_interference_actual": 140,
"task_rbf_excl_tsk_bounds_task_workload_excl_j": 69
},
"./model/schedule/uni/limited/busy_interval.v": {
"busy_interval_has_uninterrupted_service": 84,
"busy_interval_is_bounded": 81,
"exists_busy_interval_prefix": 75,
"no_idle_time_within_non_quiet_time_interval": 76,
"pending_hp_job_exists": 73
},
"./model/schedule/uni/limited/edf/nonpr_reg/concrete_models/response_time_bound.v": {
"uniprocessor_response_time_bound_edf_with_fixed_preemption_points": 168,
"uniprocessor_response_time_bound_edf_with_floating_nonpreemptive_regions": 81
},
"./model/schedule/uni/limited/edf/nonpr_reg/response_time_bound.v": {
"priority_inversion_is_bounded": 56,
"priority_inversion_is_bounded_by_blocking": 58
},
"./model/schedule/uni/limited/edf/response_time_bound.v": {
"A_is_in_concrete_search_space": 85,
"instantiated_task_interference_is_bounded": 163
},
"./model/schedule/uni/limited/fixed_priority/nonpr_reg/concrete_models/response_time_bound.v": {
"uniprocessor_response_time_bound_fp_with_fixed_preemption_points": 168,
"uniprocessor_response_time_bound_fp_with_floating_nonpreemptive_regions": 81
},
"./model/schedule/uni/limited/fixed_priority/nonpr_reg/response_time_bound.v": {
"priority_inversion_is_bounded": 52
},
"./model/schedule/uni/limited/fixed_priority/response_time_bound.v": {
"instantiated_task_interference_is_bounded": 47
},
"./model/schedule/uni/limited/jlfp_instantiation.v": {
"cumulative_task_interference_split": 62,
"instantiated_cumulative_interference_of_hep_jobs_equal_total_interference_of_hep_jobs": 114,
"instantiated_cumulative_interference_of_hep_tasks_equal_total_interference_of_hep_tasks": 127,
"instantiated_quiet_time_equivalent_edf_quiet_time": 102
},
"./model/schedule/uni/limited/platform/limited.v": {
"model_with_fixed_preemption_points_is_model_with_bounded_nonpreemptive_regions": 83
},
"./model/schedule/uni/limited/platform/priority_inversion_is_bounded.v": {
"=>": 119,
"not_quiet_implies_exists_scheduled_hp_job_after_preemption_point": 55,
"not_quiet_implies_exists_scheduled_hp_job_at_preemption_point": 90,
"scheduling_of_any_segment_starts_with_preemption_time": 44
},
"./model/schedule/uni/limited/platform/util.v": {
"belonging_to_segment_of_seq_is_total": 46,
"distance_between_neighboring_elements_le_max_distance_in_seq": 43,
"domination_of_distances_implies_domination_of_seq": 58,
"max_distance_in_nontrivial_seq_is_positive": 127,
"max_distance_in_seq_le_last_element_of_seq": 47,
"max_of_dominating_seq": 47
},
"./model/schedule/uni/nonpreemptive/schedule.v": {
"j_is_not_scheduled_at_t_minus_service_minus_one": 54,
"j_is_scheduled_at_t_minus_service": 74
},
"./model/schedule/uni/service.v": {
"all_jobs_have_completed_impl_workload_eq_service": 44,
"incremental_service_during": 70
},
"./model/schedule/uni/susp/build_suspension_table.v": {
"suspension_duration_matches_predicate_up_to_t_max": 95
},
"./model/schedule/uni/susp/last_execution.v": {
"last_execution_idempotent": 41,
"same_service_implies_same_last_execution": 49
},
"./model/schedule/uni/susp/suspension_intervals.v": {
"cumulative_suspension_eq_total_suspension": 86,
"cumulative_suspension_le_total_suspension": 57
},
"./model/schedule/uni/sustainability.v": {
"weak_sustainability_equivalence": 50
},
"./util/div_mod.v": {
"divSn_cases": 54
},
"./util/list.v": {
"subseq_leq_size": 52
},
"./util/step_function.v": {
"exists_intermediate_point": 43
},
"./util/sum.v": {
"sum_majorant_eqn": 40
}
}
}
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment