3 ms·

> If you're not verifying the actual code, then how do you prevent bugs creeping during whatever happens between verification and actually writing the applicat

by hwayne 7y ago

> If you're not verifying the actual code, then how do you prevent bugs creeping during whatever happens between verification and actually writing the application code? Code review! So, SO much code review. Also testing and type systems and linters and code review. (There's also some work on automatic synthesis, like PGo, but that's all very, very far from being production-ready.) The main benefit of using TLA+ is that it lets you hammer out issues in the high-level design. Less "oops this has a buffer overrun" and more "oops if this service stalls out for too long our recovery mechanism will violate a core safety guarantee." Turns out that lots of the nastiest bugs are in the design, not the implementation, so using TLA+ saves a lot of time and money. But you still need to code review!

0xffff2 7y ago
>Less "oops this has a buffer overrun" and more "oops if this service stalls out for too long our recovery mechanism will violate a core safety guarantee." Yeah, but we already have processes to manage the latter. It's the (potential) buffer overruns that keep me up at night! >Turns out that lots of the nastiest bugs are in the design, not the implementation I'm not saying it never happens (does TLA plus make sure everyone's assuming SI units?), but that hasn't been my experience at all.
- hwayne 7y ago
  > Yeah, but we already have processes to manage the latter. It's the (potential) buffer overruns that keep me up at night! I'd _hope_ you'd have those processes, working on space flight and all :P. Good processes > good tools. It's easier to start using a good tool than overhaul your process. So for people who don't have that kind of discipline or heavyweight process, TLA+ gives a lot of benefits for really cheap. AWS, for example, found it really easy to slot into their workflow. Re buffer overruns, I just remembered OpenComRTOS, which used TLA+ to verify low-level properties of their code.[1] They found it super helpful. > I'm not saying it never happens (does TLA plus make sure everyone's assuming SI units?), but that hasn't been my experience at all. 'Fraid it probably can't help you with the SI units. I'm thinking about "design bugs" more like this: > 1. Suppose we have a document with version 57 > 2. A bulk of delete and reindex will remove the index-v57, increase the version to 58 (for the delete operation), then put a new doc with version 59. While the engine places the index-59 into the version map, the safe-access flag is flipped over (due to a concurrent fresh), the engine won't put that index entry into the version map, but also leave the delete-58 tombstone in the version map. The delete-58 tombstone is stale because the latest version of that document is index-59. > 3. Another bulk of delete and reindex will increase the version to 59 (for a delete) but won't remove docs from Lucene because of the existing (stale) delete-58 tombstone. The index operation will append document (version 60) to Lucene (instead of overwriting). At this point, we will have two documents with the same id. Which was a bug TLA+ found in ElasticSearch.[2] [1]: https://dl.acm.org/doi/10.5555/1779934.1779955 https://dl.acm.org/doi/10.5555/1779934.1779955 [2]: https://github.com/elastic/elasticsearch/issues/31976#issuecomment-404722753 https://github.com/elastic/elasticsearch/issues/31976#issuec...

by hwayne 7y ago

0xffff2 7y ago

>Less "oops this has a buffer overrun" and more "oops if this service stalls out for too long our recovery mechanism will violate a core safety guarantee." Yeah, but we already have processes to manage the latter. It's the (potential) buffer overruns that keep me up at night! >Turns out that lots of the nastiest bugs are in the design, not the implementation I'm not saying it never happens (does TLA plus make sure everyone's assuming SI units?), but that hasn't been my experience at all.

hwayne 7y ago
> Yeah, but we already have processes to manage the latter. It's the (potential) buffer overruns that keep me up at night! I'd _hope_ you'd have those processes, working on space flight and all :P. Good processes > good tools. It's easier to start using a good tool than overhaul your process. So for people who don't have that kind of discipline or heavyweight process, TLA+ gives a lot of benefits for really cheap. AWS, for example, found it really easy to slot into their workflow. Re buffer overruns, I just remembered OpenComRTOS, which used TLA+ to verify low-level properties of their code.[1] They found it super helpful. > I'm not saying it never happens (does TLA plus make sure everyone's assuming SI units?), but that hasn't been my experience at all. 'Fraid it probably can't help you with the SI units. I'm thinking about "design bugs" more like this: > 1. Suppose we have a document with version 57 > 2. A bulk of delete and reindex will remove the index-v57, increase the version to 58 (for the delete operation), then put a new doc with version 59. While the engine places the index-59 into the version map, the safe-access flag is flipped over (due to a concurrent fresh), the engine won't put that index entry into the version map, but also leave the delete-58 tombstone in the version map. The delete-58 tombstone is stale because the latest version of that document is index-59. > 3. Another bulk of delete and reindex will increase the version to 59 (for a delete) but won't remove docs from Lucene because of the existing (stale) delete-58 tombstone. The index operation will append document (version 60) to Lucene (instead of overwriting). At this point, we will have two documents with the same id. Which was a bug TLA+ found in ElasticSearch.[2] [1]: https://dl.acm.org/doi/10.5555/1779934.1779955 https://dl.acm.org/doi/10.5555/1779934.1779955 [2]: https://github.com/elastic/elasticsearch/issues/31976#issuecomment-404722753 https://github.com/elastic/elasticsearch/issues/31976#issuec...