opened
merge request
!383
"Draft: Add Suspension definition and related lemmas"
at
RT-PROOFS / PROSA - Formally Proven Schedulability Analysis
closed
merge request
!379
"add overhead aware proc state"
at
RT-PROOFS / PROSA - Formally Proven Schedulability Analysis
accepted
merge request
!382
"vacuum vok and vos files"
at
RT-PROOFS / PROSA - Formally Proven Schedulability Analysis
opened
merge request
!382
"vacuum vok and vos files"
at
RT-PROOFS / PROSA - Formally Proven Schedulability Analysis
opened
merge request
!381
"Draft: Add RTA for exceedance"
at
RT-PROOFS / PROSA - Formally Proven Schedulability Analysis
accepted
merge request
!378
"add processor state for exceedance analysis"
at
RT-PROOFS / PROSA - Formally Proven Schedulability Analysis
commented on
merge request !378
"add processor state for exceedance analysis"
at
RT-PROOFS / PROSA - Formally Proven Schedulability Analysis
Thanks for the proof improvements!
commented on
merge request !378
"add processor state for exceedance analysis"
at
RT-PROOFS / PROSA - Formally Proven Schedulability Analysis
It says this was applied, but somehow it's not showing in the diff.
commented on
merge request !378
"add processor state for exceedance analysis"
at
RT-PROOFS / PROSA - Formally Proven Schedulability Analysis
Looks good. The proofs could be a lot shorter in ssreflect style, but I'm not going to bother to rewrite them.
approved
merge request
!378
"add processor state for exceedance analysis"
at
RT-PROOFS / PROSA - Formally Proven Schedulability Analysis
commented on
merge request !378
"add processor state for exceedance analysis"
at
RT-PROOFS / PROSA - Formally Proven Schedulability Analysis
Is this actually necessary in this section?
commented on
merge request !378
"add processor state for exceedance analysis"
at
RT-PROOFS / PROSA - Formally Proven Schedulability Analysis
| ExceedanceExecution _ => true...
commented on
merge request !378
"add processor state for exceedance analysis"
at
RT-PROOFS / PROSA - Formally Proven Schedulability Analysis
(** In this section, we consider any type of jobs. *)
commented on
merge request !378
"add processor state for exceedance analysis"
at
RT-PROOFS / PROSA - Formally Proven Schedulability Analysis
service, i.e., it provides at most one unit of service at any time instant. *)
commented on
merge request !378
"add processor state for exceedance analysis"
at
RT-PROOFS / PROSA - Formally Proven Schedulability Analysis
consuming, i.e., all the supply offered is consumed by the scheduled job. *)
commented on
merge request !378
"add processor state for exceedance analysis"
at
RT-PROOFS / PROSA - Formally Proven Schedulability Analysis
model, i.e., only one job can be scheduled at any time instant. *)
commented on
merge request !378
"add processor state for exceedance analysis"
at
RT-PROOFS / PROSA - Formally Proven Schedulability Analysis
Lemma scheduled_at_procstate (sched : schedule (exceedance_proc_state Job)) j t :...
accepted
merge request
!375
"Add RS ELF RTA for preemption models"
at
RT-PROOFS / PROSA - Formally Proven Schedulability Analysis