Verifying for all interlacings

A prospective user experimenting with Frama-C wonders whether it is possible to verify the behavior of an interrupt-driven system for all possible interlacing of interrupts.

We assume, for now, that interrupts are themselves uninterruptible. The prospective user wants to verify that nothing wrong happens when each interrupt is called once, in any order. He wrote the analysis context below.

void test_case1(void)
{
	main();
	interrupt_device1();
	interrupt_device2();
	interrupt_device3();
}
void test_case2(void)
{
	main();
	interrupt_device1();
	interrupt_device3();
	interrupt_device2();
}
void test_case3(void)
{
	main();
	interrupt_device2();
	interrupt_device1();
	interrupt_device3();
}
void test_case4(void)
{
	main();
	interrupt_device2();
	interrupt_device3();
	interrupt_device1();
}
void test_case5(void)
{
	main();
	interrupt_device3();
	interrupt_device1();
	interrupt_device2();
}
void test_case6(void)
{
	main();
	interrupt_device3();
	interrupt_device2();
	interrupt_device1();
}

Function main() does a bit of initialization. Each of the functions test_case1(), …, test_case6() is used as an entry point for the value analysis.

This method works: studying the six entry points one after the other, properties about many possible executions can be found. The problem is that this method does not scale well to larger numbers of interrupts.

The next post will answer two questions, that I invite you to think about for yourself. Note that the writing of analysis contexts is mostly orthogonal to the careful selection of options and annotations that help the value analysis conclude to the safety of the code. This is why I am suggesting these exercises without offering the code of interrupt_device1(), …, interrupt_device3(). Only in the most difficult cases (as happened for the verification of the strongest properties for Skein-256) is it necessary to adapt the analysis context to make the verification possible. By the same token proofreading a verification in order to check that the right property was verified usually only means proofreading the analysis context not the options and annotations that enabled the value analysis to reach its conclusion. Most options are safe to use and the value analysis tells whether it uses a user annotation as an assumption or only as a hint.

Here are the questions the next post will focus on:

1. What shorter analysis context would test exactly the same behaviors as the six entry points above in a single analysis?
2. What shorter analysis context would test arbitrarily long sequences of interrupts with repetitions?