From 3b689961f55a23e9202cab16157e9c71b8d7f9fe Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Bj=C3=B6rn=20Brandenburg?= Date: Mon, 24 Jun 2019 17:49:35 +0200 Subject: [PATCH] enable proof-length checking during CI --- .gitlab-ci.yml | 6 + scripts/known-long-proofs.json | 314 +++++++++++++++++++++++++++++++++ 2 files changed, 320 insertions(+) create mode 100644 scripts/known-long-proofs.json diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 12dd5bf1..1e15747f 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -70,3 +70,9 @@ doc: - "with-proofs/" - "without-proofs/" 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` diff --git a/scripts/known-long-proofs.json b/scripts/known-long-proofs.json new file mode 100644 index 00000000..ad88b329 --- /dev/null +++ b/scripts/known-long-proofs.json @@ -0,0 +1,314 @@ +{ + "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 + } + } +} -- GitLab