Johnson's procedure: mechanization and parallelization

M Filali (1, 2) , Nabil Zaidi (3)

1 IRIT-ACADIE - Assistance à la Certification d’Applications DIstribuées et Embarquées
2 CNRS - Centre National de la Recherche Scientifique
3 Lycée Blaise Pascal

In this note, we present a mechanization of Johnson’s procedure. We first specify the scheduling problem, we are concerned with. Then, we formalize Johnson’s procedure and prove an invariant. Thanks to this invariant, we prove the correctness of Johnson’s procedure and its optimality. Last, also thanks to the invariant, we elaborate a concurrent version of Johnson’s procedure which is correct by construction. We use the Python language for expression and experimentation purposes. The Isabelle HOL assistant theorem prover is used for validating the correctness.

Mots clés: Real-time scheduling

Domaines: Génie logiciel [cs.SE]; Systèmes embarqués; Cryptographie et sécurité [cs.CR]; Interface homme-machine [cs.HC]; Architectures Matérielles [cs.AR]; Modélisation et simulation

M Filali, Nabil Zaidi. Johnson's procedure: mechanization and parallelization. 7th International Real-Time Scheduling Open Problems Seminar (RTSOPS 2016) in conjunction with ECRTS 2016, Jul 2016, Toulouse, France. pp.9-10. ⟨hal-01517378⟩