3 ms·
> One of the errors found with SPIN, a missing critical section around a conditional wait statement, was in fact reintroduced in a different subsystem that was
by brokenmachine 9y ago
> One of the errors
found with SPIN, a missing critical section around a
conditional wait statement, was in fact reintroduced in a
different subsystem that was not verified in this first preflight
effort. This error caused a real deadlock in the RA
during flight in space.
So they used code that they had already discovered an error in, in a different subsystem. I would not contend that that means that software verification doesn't work.
- lisper 9y agoThat sentence is not a completely accurate account of what happened. The error was not in a "different subsystem", it was in the same subsystem as the verified code: the executive. The code was structured as a verified kernel with unverified application code written on top of it. The verification proved that the code would be free of deadlocks if the application code used the kernel operations exclusively, and did not directly use any primitives like mutexes, but it turned out that this design rule was violated.