Software with timers and clocks (STACs) exchange clock values to set timers and perform computation. STACs are key elements of safety-critical systems that make up the infrastructure of our daily lives. They are particularly used to control systems that interact (and must be synchronized) with the physical world. Examples include avionics systems, medical devices, cars, cell phones, and other devices that rely on software not only to produce the right output, but also to produce it at the correct time. An airbag, for example, must deploy as intended, but just as importantly, it must deploy at the right time. Thus, when STACs fail to operate as intended in the safety-critical systems that rely on them, the result can be significant harm or loss of life. Within the Department of Defense (DoD), STACs are used widely, ranging from real-time thread schedulers to controllers for missiles, fighter planes, and aircraft carriers. This blog post presents exploratory research to formally verify safety properties of sequential and concurrent STACs at the source-code level.

The Challenges of Formal Verification

The operating system (OS), which manages different resources, different threads, and different processes, is at the heart of all software. The OS relies on a scheduler for allocating the appropriate amount of processor time to all these threads (i.e., tasks). We are concerned here with real-time threads, i.e., those with periodically executing jobs that have hard deadlines. Processor time is a scarce resource that must be allocated properly so that every job completes by its deadline.

For real-time systems, the thread scheduler is critical and must be correct, not only in scheduling the threads correctly but also in ensuring that they are scheduled at the right time. In particular, these tasks are relegated to a class of thread schedulers that are also doing time enforcement, which is also known as budget enforcement. These thread schedulers ensure that a certain thread does not receive more processor time than needed, a critical function. For example, in an automobile, if the thread scheduler in a vehicle's system allocates too much processor time to the cruise control software, the electronic stability control software might fail to prevent the car from understeering (not turning fast enough) in a curve.

The goal of this research is to verify real-time enforcers, or timing enforcers, exhaustively in a mathematically formal way. More importantly, we want to do this verification at the source code level. For example, given C source code for a scheduler or enforcer, we want to prove that it schedules the threads correctly (e.g., respecting priorities) but also that it performs timing budget enforcement at the right time (i.e., stopping a thread just before it exceeds its allotted processor time).

As outlined in our recently published paper, Contract-Based Verification of Timing Enforcers, several factors complicate STACs verification:

• The semantics of STACs involve time. Timers and clocks are implemented by an OS subsystem that tracks time using special hardware (e.g., High Precision Event Timer and the time-stamp counters). The behavior of this subsystem must therefore be modeled soundly.
  
  
• STACs can behave incorrectly. Due to numeric overflows, STACs can violate monotonicity of timestamps maintained in variables with finite domain types, such as int.
  
  
• STACs use pointers and memory operations substantially since they are often high-performance system software. For example, a scheduler typically maintains active threads as a linked list, which is dynamically updated as threads are created and destroyed. Verifying correctness of pointer-manipulating programs is known to be challenging for software verification tools.

While there have been previous efforts, these efforts have been restricted mainly to models (e.g., using timed automata and associated model checkers, such as UPPAAL.) Our goal with this research is to verify STAC systems at the source-code level, thereby reducing the semantic gap between what is verified and what is executed.

Our Approach

To verify systems at the source-code level, the scheduler essentially relies on timers. In single-processor systems, when the application threads are running, the OS by default cannot run. A separate timer mechanism in hardware must ensure that the thread is stopped, and the OS is given back control.

Through our research, we are working to ensure that these timers are being used correctly, which can be complicated for many reasons:

• Numerical overflow. Even though time is unbounded, in software, time stamps or time values are represented by variables with finite domain types, such as int. Similar to the Y2K problem, when the value of such a variable increases beyond the upper bound of the type, it wraps over and goes from a high value to a low value, violating the monotonicity of time. Underflows can also happen due to numeric computations, e.g., the result of a subtraction can be larger than the first argument.

• Budget enforcement. During budget enforcement, to compute when the timer should be set, the scheduler performs various numeric operations, such as subtraction, addition, and multiplication, over timestamp values. Again, we must verify that these operations are performed carefully to avoid numeric overflows and underflows. Otherwise, they will lead to incorrect behavior.

• Measurement precision. How does the software know what the current time is? A hardware clock counter reads the clock counter value, which is automatically updated by the hardware. While the software can read the value of the hardware clock counter, this inherently results in a measurement precision issue. The value that the software reads is, by definition, already outdated by a few nanoseconds (There is no instantaneous action in this universe, as far as we know).

When attempting to write software programs, specifically software for safety-critical embedded systems, developers must take these challenges into account.

Applying Theorem Proving to Software

To verify STACs at the code-base level, we rely on deductive verification and essentially applying theorem proving to software. We are using a tool called Frama-C, which is a publicly available source-code analysis tool, for deductive verification for C source code.

Even though Frama-C is a source-code analysis tool, we still needed to manually specify function contracts and loop variants using the ACSL language. Frama-C checks automatically that these contracts and invariants are valid by constructing verification conditions and discharging them using backend satisfiability modulo theory (SMT) solvers. Thus, by automating the tedious parts of the process, Frama-C makes deductive verification applicable to software of realistic complexity.

Verifying Zero Slack Rate Monotonic Scheduling

To verify a specific time real-time enforcer, we target the scheduler for zero slack rate monotonic (ZSRM), a type of fixed priority thread-scheduling technique for mixed-criticality systems. To put it more simply, ZSRM schedules the threads that execute a specific function periodically.

Given a set of threads with different levels of criticality (e.g., in an automobile, an engine control thread will have high criticality, while an audio player thread will have low criticality) ZSRM ensures that under overload conditions, preference is given to threads with higher criticality over those with lower criticality. Under nominal (i.e., non-overload) conditions, ZSRM uses rate-monotonic scheduling.

We plan to verify the following three qualities:

• That the threads that are ready to run are ordered in the right priority. This means that we will use parameters to establish a priority in the thread scheduler. Another parameter of the thread is the interval of time, or budget, it will be allowed to run. Preemption occurs when another thread with higher priority than the one that is running gets ready to execute. The thread with higher priority will interrupt the currently running thread, a pattern known as periodic activation that is common in real-time systems.
  
  In the code, there is a linked list of all the threads that are active with their priorities. It is important to be able to show that the linked list is always maintained in the correct sorted order (i.e., the tread at the top of the linked list, which will be next in line for execution, is the thread with the highest priority.
  
  Two actions result in modification of the list:

When a new thread goes to sleep, it does so because it has already executed and does not need to run anymore.

When the thread wakes up again and must execute, it will be added to the list.

• That the budget that is being consumed is being updated properly. This means the variable that is counting the time a thread is running in the processor is updated correctly even when it is interrupted by higher-priority tasks.
  
  
• That the timer used to enforce the processor time budget is correctly programmed. Specifically, timers are implemented as a specialized circuit that decrements a variable (by one) at regular intervals (say every 1 nanosecond). Once the variable reaches zero, it sends an interrupt to the processor that executes a special function (known as timer interrupt). To properly enforce the budgets, the scheduler must perform the proper calculation to set up the timer variable with the correct interval taking into account the implicit imprecision of the clocks and delays to start executing the timer interrupt.

A Foundation in Deductive Verification

We are basing our approach on deductive verification, which was introduced by Robert Floyd and Tony Hoare, as a way of reasoning about a program's correctness based on logical assertions. A central tenet of Hoare's logic is the Hoare triple:

To check if the above claim is valid, it is necessary to construct a logical formula called verification condition.

Floyd, also from Carnegie Mellon University, focused on creating verification conditions for programs without loops (i.e., straight code). Hoare, who thought of programming languages without pointers and aliasing, extended Floyd's approach to reason about programs, with loops and function calls, an extension known as Floyd-Hoare logic.

Although the premise remains the same, in the last 30 years the ideas introduced by Floyd and Hoare have matured into tools, such as Frama-C. Now, to verify ZSRM, pre/post conditions are written for code, often across function calls. Essentially, for a function, the precondition specifies that the state (values of arguments and global variables) under which it must be invoked, while the post-condition specifies the state (values of global variables and the return value, if any) under which it terminates.

We also specify a loop invariant for each loop, which is a condition that must be true just prior to the execution of the loop body. Given the pre/post conditions of functions, and the looping variants, Frama-C produces all the verification conditions and proves them using SMT solvers. It also interprets the results from the SMT solvers to provide diagnostic feedback in case a verification condition is found to be invalid.

Wrapping Up and Looking Ahead

Through our work, we have learned a lot about the limitations and powers of Frama-C. Initially, we implemented a simpler version of ZSRM, and verified the first two qualities: that the threads are in the correct order according to priority and that budgets are computed correctly.

More recently, we focused on transitioning to the fuller version ZSRM implemented as a Linux kernel module, and adding back some of the missing components in the source code. Our aim is to make it easier for us to transition this work to the public (a kernel module is the standard for contributing to the Linux community). We are working toward a public release of the ZSRM source code with full ACSL annotations.

By demonstrating higher assurance about well-defined pieces of software infrastructure, users will have overall higher confidence that the system will perform as designed. Our approach is also reproducible. The function contracts and loop variants are specified in the C code via ACSL annotations. Syntactically, all ACSL annotations are "comments" from the point of view of C. Thus, while these comments are ignored by a C compiler, and do not affect the meaning of the program, users of the code can read and understand the annotations, and re-verify them using Frama-C.

Another benefit that we have noted as a result of the verification is that if software developers understand that their code will be verified using Frama-C or another deductive verifier, they will structure it in such a way so that it becomes more understandable and verifiable. Instead of writing very complex "spaghetti code," developers provide a more elegant structure with well-designed loops and functions.

Once the proof is complete, these loop variants and pre/post conditions will let users know exactly

• what a specific function is supposed to execute
• under what condition is it supposed to be called
• what can be expected when it is complete

Providing this type of feedback is one of the aims of formal verification, to make programs clean and modular and understandable and well documented. In some sense, the Frama-C contracts are the best kind of documents because there is no ambiguity, and they offer a single interpretation that proves very powerful. We are also using ZSRM in a separate research project looking at Distributed Adaptive Real-Time Systems, so the results of this research benefit that project as well.

We welcome your feedback on this research in the comments section below.

Additional Resources

Read the paper Contract-Based Verification of Timing Enforcers, which was presented at ACM SIGAda's High Integrity Language Technology International Workshop on Model-Based Development and Contract-Based Programming (HILT), October 6-7, 2016, Pittsburgh, PA, USA.

For more information on ZSRM, view the 2009 paper On the Scheduling of Mixed-Criticality Real-Time Tasksets by Dionisio de Niz, Karthik Lakshmanan, and Raj Rajkumar.