formal verification

2 Articles

Reflecting On A Queueing Prism Leads To Unexpected Results

May 7, 2022 by 6 Comments

Computers are difficult enough to reason about when there’s just a single thread doing one task. There are dozens of cores in today’s modern processor world, and your program might try to take advantage of using more than just one. Things happening concurrently makes the number of states and interactions explode in to a mess we as humans are likely going to have trouble understanding. So, like [Hillel], you might turn to the computer to try and model those interactions.

The model in question is a task queue. Things are added to the pile, and “workers” grab one from the pile and process it. There are two metrics used to measure the effectiveness of a task queue: throughput and latency. Throughput is the number of things you can do per second (like this maximum throughput 3d printer), while latency is the amount of time it takes to finish one thing. Continue reading “Reflecting On A Queueing Prism Leads To Unexpected Results” →

Can You Trust Your C Compiler?

January 24, 2019 by 57 Comments

If you are writing a hello world program, you probably aren’t too concerned about how the compiler translates your source code to machine code. However, if your code runs on something that people’s lives depend on, you will want to be a bit pickier and use something like the COMPCERT compiler.  It’s a formally verified compiler, meaning there is a mathematical proof that what you write in C will be correctly translated to machine code. The compiler can generate for PowerPC, ARM, RISC-V, and x86, accepting a subset of ISO C 99 with a few extensions. While it doesn’t produce code that runs as fast as gcc, you can be sure the generated code will do what you asked it to do.

Of course, this still provides no assurance that your code will work. It just means that if you write something such as “x=0;” the generated code will set x to zero and will not do anything else. You can apply formal methods to verify your source code and be assured that the compiler doesn’t introduce possible failures. Cases where code like “x=0;” does extra things or incorrect things are very hard to figure out because the source code is correct and an examination of the generated code would be necessary to find the compiler’s code generation bug.

Continue reading “Can You Trust Your C Compiler?” →