4 ms·

> So you're saying humans are bad at writing software, but good at writing translations for model checkers? Nice strawman. However, that's not at all what I sa

> So you're saying humans are bad at writing software, but good at writing translations for model checkers? Nice strawman. However, that's not at all what I said. To restate in different words, even proofs can be incorrect. Even model checkers can be wrong. However, you seem to be under the impression that unless a model checker is 100% perfect, it's worthless. That's not the case. For the vast majority of situations, the model checker will either correctly generate a constraint problem based on what you provide (remember, garbage in / garbage out and proofs of bad theorems are meaningless), or will generate some kind of diagnostic error. Everything -- EVERYTHING -- is flawed. But, if your standard of measure is "only perfect things can augment or replace unit tests" then you're doing yourself and any organization you contribute to a great disservice. > I am aware, trust me. Respectfully, I think you're still conflating model checkers, static analyzers, and proof systems. > Are you aware how much effort they had to expend to do that? Clearly, much less than you think. I've estimated both ways. Using CBMC adds 30% overhead. That's well worth the effort.

gavinhoward 3y ago
> However, you seem to be under the impression that unless a model checker is 100% perfect, it's worthless. That's not the case. Unfortunately, unless you're careful, or have a test suite to make sure, it is the case. You might have a good model, but if your software doesn't actually implement the model, it's giving you a false sense of security. And those bugs can persist. > Respectfully, I think you're still conflating model checkers, static analyzers, and proof systems. Not at all. I know the differences. But in this context, they all have the same problem: making sure the code matches the model/proof (static analyzers have an implicit internal model). > Clearly, much less than you think. I've estimated both ways. Using CBMC adds 30% overhead. That's well worth the effort. Ten years of work for four people, I think. That's not 30% overhead. I think at last count, their C code was less than 10 KLoC, but their proof was beyond 200-300 KLoC. That's a 2000% overhead.
- nanolith 3y ago
  > Unfortunately, unless you're careful, or have a test suite to make sure, it is the case. Respectfully, you are definitely conflating these concepts. First, a test suite can't replace a model checker. These are two very different things. You can absolutely miss things in a test suite, and even get 100% branch coverage. Your tests can appear to be perfect, and can even pass code review, and still miss things. A test suite can't make sure of anything, because this would imply that your software and your test suite is perfect. Unit testing is empirical. Not model driven or constructive. Hence, you don't actually have any indication about when you are done. Even if you get to 100% branch coverage. Even if your tests appear to be perfect. You have likely missed tests that exercise cases in your code that you don't even realize are there. Undefined behavior due to integer overflow is common, and almost every mature code base that I have seen -- including SQLite -- misses these classes of errors. A model checker or a constructive proof system starts from a priori theory. This is used to extract software, or in the case of a source level model checker, the software is used to create the model. While it is certainly possible for gaps to exist here, it's far less likely. Furthermore, there is a direct way to translate this a priori knowledge into "done". If the model checker uses the same libraries as the code generator in the compiler, then there can be a 1:1 relationship between the constructed model and the generated code. Barring inaccuracies in hardware simulation or actual hardware errors or compiler errors, the two will be quite close. If the compiler were extracted from constructive proofs (e.g. CompCert), then the likelihood of compiler errors generating different machine code is even further removed. While nothing is perfect, we are talking about two to three orders of magnitude of added precision over hand-written unit tests. > You might have a good model, but if your software doesn't actually implement the model... Ah... there's part of the problem. You don't seem to understand what a model checker is. A model checker transforms source code into a constraint solver, following the same rules that the compiler uses to generate machine code. Yes, there are high-level model checkers that can work on algorithms, but as is clear from the context, I'm talking about source level model checkers. The software and the model are the same. The model is based on the same abstract machine model used for the language and for the particular machine code implementation. The software is transformed into a constraint solver on top of this model. If the two don't match, then a lot of things have gone seriously wrong. In practice, this is about as likely as your compiler generating the wrong code, or your CPU deciding that the MOV instruction really means JMP. > Not at all. I know the differences. Clearly not, and here's why: > Ten years of work for four people, I think... That's a 2000% overhead. The seL4 team used constructive proof assistant (i.e. Isabelle HOL). Not a model checker (e.g. CBMC). You're conflating the two. You don't understand the difference, and you're plunging ahead as if you do. That is where the crux of this disagreement comes from. Model checkers and constructive proof assistants are both ways to do formal methods, but they are different, with different use cases. seL4 is an atypical example, which used pure constructive proofs because they needed to prove that their operating system implemented well founded process isolation. When I mentioned that the seL4 team used a model checker, I meant and implied, IN ADDITION TO the constructive proof assistant. This is because both systems are best used for different domains. In practice, the use of a model checker requires relatively minimal overhead. In practice -- my use case -- this is around 30%. Respectfully, I think you should spend some time studying and using these tools. They will improve the quality of the software you write.

gavinhoward 3y ago

> However, you seem to be under the impression that unless a model checker is 100% perfect, it's worthless. That's not the case. Unfortunately, unless you're careful, or have a test suite to make sure, it is the case. You might have a good model, but if your software doesn't actually implement the model, it's giving you a false sense of security. And those bugs can persist. > Respectfully, I think you're still conflating model checkers, static analyzers, and proof systems. Not at all. I know the differences. But in this context, they all have the same problem: making sure the code matches the model/proof (static analyzers have an implicit internal model). > Clearly, much less than you think. I've estimated both ways. Using CBMC adds 30% overhead. That's well worth the effort. Ten years of work for four people, I think. That's not 30% overhead. I think at last count, their C code was less than 10 KLoC, but their proof was beyond 200-300 KLoC. That's a 2000% overhead.

nanolith 3y ago
> Unfortunately, unless you're careful, or have a test suite to make sure, it is the case. Respectfully, you are definitely conflating these concepts. First, a test suite can't replace a model checker. These are two very different things. You can absolutely miss things in a test suite, and even get 100% branch coverage. Your tests can appear to be perfect, and can even pass code review, and still miss things. A test suite can't make sure of anything, because this would imply that your software and your test suite is perfect. Unit testing is empirical. Not model driven or constructive. Hence, you don't actually have any indication about when you are done. Even if you get to 100% branch coverage. Even if your tests appear to be perfect. You have likely missed tests that exercise cases in your code that you don't even realize are there. Undefined behavior due to integer overflow is common, and almost every mature code base that I have seen -- including SQLite -- misses these classes of errors. A model checker or a constructive proof system starts from a priori theory. This is used to extract software, or in the case of a source level model checker, the software is used to create the model. While it is certainly possible for gaps to exist here, it's far less likely. Furthermore, there is a direct way to translate this a priori knowledge into "done". If the model checker uses the same libraries as the code generator in the compiler, then there can be a 1:1 relationship between the constructed model and the generated code. Barring inaccuracies in hardware simulation or actual hardware errors or compiler errors, the two will be quite close. If the compiler were extracted from constructive proofs (e.g. CompCert), then the likelihood of compiler errors generating different machine code is even further removed. While nothing is perfect, we are talking about two to three orders of magnitude of added precision over hand-written unit tests. > You might have a good model, but if your software doesn't actually implement the model... Ah... there's part of the problem. You don't seem to understand what a model checker is. A model checker transforms source code into a constraint solver, following the same rules that the compiler uses to generate machine code. Yes, there are high-level model checkers that can work on algorithms, but as is clear from the context, I'm talking about source level model checkers. The software and the model are the same. The model is based on the same abstract machine model used for the language and for the particular machine code implementation. The software is transformed into a constraint solver on top of this model. If the two don't match, then a lot of things have gone seriously wrong. In practice, this is about as likely as your compiler generating the wrong code, or your CPU deciding that the MOV instruction really means JMP. > Not at all. I know the differences. Clearly not, and here's why: > Ten years of work for four people, I think... That's a 2000% overhead. The seL4 team used constructive proof assistant (i.e. Isabelle HOL). Not a model checker (e.g. CBMC). You're conflating the two. You don't understand the difference, and you're plunging ahead as if you do. That is where the crux of this disagreement comes from. Model checkers and constructive proof assistants are both ways to do formal methods, but they are different, with different use cases. seL4 is an atypical example, which used pure constructive proofs because they needed to prove that their operating system implemented well founded process isolation. When I mentioned that the seL4 team used a model checker, I meant and implied, IN ADDITION TO the constructive proof assistant. This is because both systems are best used for different domains. In practice, the use of a model checker requires relatively minimal overhead. In practice -- my use case -- this is around 30%. Respectfully, I think you should spend some time studying and using these tools. They will improve the quality of the software you write.