4 ms·
Intel uses TLA+ extensively for formal verification of its subsystems, in a kind of piecemeal approach. Famously, a Microsoft intern modeled the XBox's cache c
by sterlind 8y ago
Intel uses TLA+ extensively for formal verification of its subsystems, in a kind of piecemeal approach.
Famously, a Microsoft intern modeled the XBox's cache coherence protocol and caught a bug there before they went to prod.
Certainly bit flips can happen, but you can still prove that circuits obey your invariants!
(Note: TLA+ doesn't always fully prove correctness. Z3 is a more sophisticated approach but harder to apply to temporal logic)
- baybal2 8y ago>Famously, a Microsoft intern modeled the XBox's cache coherence protocol and caught a bug there before they went to prod. xdcbt bug?
- sterlind 8y agoDifferent bug! Good guess, though. http://channel9.msdn.com/Events/Build/2014/3-642#time=21m46s http://channel9.msdn.com/Events/Build/2014/3-642#time=21m46s > A little closer to home, Lamport shared an anecdote of how his programming language even helped Microsoft avert a near-certain disaster. While writing a TLA+ specification for an IBM-developed memory system chip in the Xbox 360, a Microsoft intern discovered a bug that would cripple the game console. The IBM engineers’ first reactions were of disbelief, saying it could not possibly happen, Lamport said. However, they changed their tune a few weeks later. “Their tests would not have discovered it, and had this intern not discovered this bug, it would have gone into production; every Xbox would have crashed after four hours of use. [That’s] a nice success story.” Source: https://www.asianscientist.com/2016/01/features/gyss-2016-leslie-lamport-turing-award/ https://www.asianscientist.com/2016/01/features/gyss-2016-le...