Internship: Clock Discipline Algorithm in Coq

4 minute read

(link to the pdf.)

For more information, do not hesitate to contact me: benjamin.lion at inria.fr.

Context

“Real-time model checking is really simple.” As advertised by Leslie Lamport in [3], the real passage of time can be encapsulated explicitely in TLA+ using a now variable that increments with a Tick action. As a consequence, the model checking of real-time properties is easier, without necessarily requiring all the complex background details.

Yet, a model differs from the code that executes on a machine, unless proven otherwise. This is the main result of CompCert [2], a verified compiler for the C language, that certifies that the semantics of an executable coincides with the semantics of the source code. However, the semantic preservation theorem does not yet include real time guarrantees.

As CompCert explicitly says in its documentation, the semantic preservation theorem ensures that observable behaviours of the source and target programs are the same, and define observable behaviour as “everything the user of the program, or the physical world in which it executes, can see about the actions of the program, with the notable exception of execution time and memory consumption.”.

Challenge

In this work, we will focus on a specific time sensitive algorithm: the Clock Discipline Algorithm [6]. The algorithm synchronizes a high frequency clock that may accumulate drifting, with a low frequency clock that is reliable. Typically, this algorithm is employed to secure local time on an operating system from the source time given by an external reliable source (i.e., via NTP).

The Clock Discipline algorithm estimates the difference between the two clocks, so that a reading of the local clock can be reliably converted as a value on the source reliable clock.

We will implement this algorithm in software (in a fragment of C), and use a certified compiler to generate code. Moreover, we will prove that the bound estimations given by the algorithm, under assumption verified by the hardware, are realistic and preserved through compilation. The challenge will therefore be to port some of the existing proving technics for memory-safe programs [1], to deal with time-dependent registers (such as [5]).

Goals

The verification of the clock discipline algorithm decomposes into three main goals:

  1. Identification of a suitable formalism to formalize the Clock discipline algorithm in Coq.
    The clock discipline algorithm has time-dependent instruction. We will use a simple time model, similar to the time-stamp counter register in modern processor, to reason about correctness of the algorithm. For instance, in [6], it says that “It is possible to convert the discretized time reports of the clocks to continuous time readings by assuming that the associated counter increments once in one period, and by ignoring residual time error within one period.”

  2. Implementation of the model in a low level language, such as Clight.
    *This step requires to get familiar with the Clight syntax and its semantics. Several extensions will need to be considered, to express time syntactically and semantically, such as in [4].

  3. Practical generation of certified code on a specific plateform.
    The third objective is to setup a toolchain to generate executable and testable code on some specific architecture. Then, the performance of the generated code could be evaluated with respect to the model prediction.

The set of goals is ambitious, which implies that some of the goals might not be fully completed given the duration of the internship.

Other details {#references. unnumbered}

Practical details:

  • supervised by Benjamin Lion;
  • funded by the cert-t project;
  • gratification;
  • integration in the Epicure team at Inria Rennes.

Time plays a critical role on embedded and systems with energy constraints. As future direction, one project that may benefit from the work is the RIOT~\cite{RIOT} operating system for IoT. The verification of their internal timer library could be a possible avenue for exension, as it makes use of similar clock discipline algorithm.

References

[1]: Blazy, Sandrine, and Xavier Leroy. 2009. “Mechanized Semantics for the Clight Subset of the C Language.” CoRR abs/0901.3619. http://arxiv.org/abs/0901.3619.

[2]: CompCert. n.d. “CompCert Website.” https://compcert.org/.

[3]: Lamport, Leslie. 2005. “Real-Time Model Checking Is Really Simple.” In 13th Advanced Research Working Conference on Correct Hardware Design and Verification Methods, 13th Advanced Research Working Conference on Correct Hardware Design and Verification Methods. https://www.microsoft.com/en-us/research/publication/real-time-model-checking-is-really-simple/.

[4]: Natarajan, Saranya, and David Broman. 2018. “Timed C: An Extension to the C Programming Language for Real-Time Systems.” In IEEE Real-Time and Embedded Technology and Applications Symposium, RTAS 2018, 11-13 April 2018, Porto, Portugal, edited by Rodolfo Pellizzoni, 227–39. IEEE Computer Society. https://doi.org/10.1109/RTAS.2018.00031.

[5]: Wikipedia. n.d. “Time Stamp Counter.” https://en.wikipedia.org/wiki/Time_Stamp_Counter.

[6]: Yigitler, Hüseyin, Behnam Badihi, and Riku Jäntti. 2020. “Overview of Time Synchronization for IoT Deployments: Clock Discipline Algorithms and Protocols.” Sensors 20 (20): 5928. https://doi.org/10.3390/S20205928.