3 ms·

Keeper is tested in the same way as ClickHouse. There are Keeper only tests, but we run ClickHouse with Keeper for all of our server tests. For each test we t

Keeper is tested in the same way as ClickHouse. There are Keeper only tests, but we run ClickHouse with Keeper for all of our server tests. For each test we try to use all useful tools for verifying safety and correctness like sanitizers. E.g. an interesting tool we introduced in our codebase for thread safety https://clang.llvm.org/docs/ThreadSafetyAnalysis.html# https://clang.llvm.org/docs/ThreadSafetyAnalysis.html# We found some issues using sanitizers in our codebase and NuRaft library itself which were instantly fixed. And let's not forget about Jepsen which showed some really tricky bugs but were more related to the correctness.

nanolith 3y ago
Thanks. That is useful. I would suggest looking into CBMC and similar tools as well. Model checking is incredibly useful.
- antonio2368 3y ago
  Sadly I never put enough effort into trying out such checks. but your excitement about them gives me motivation to properly try them out.
  - nanolith 3y ago
    CBMC is subtle and will require some code changes to use effectively. The real key for using it, in my opinion, is to isolate individual classes and functions. Avoid instrumenting code with recursion and loops, and focus on defining and verifying function contracts, class invariants, and resource / memory lifetimes. It will require a significant amount of work to mock up standard library and third party library APIs, but the real beauty of CBMC is that once you define the interface contracts for these APIs and libraries, you can verify every use of them. I used CBMC previously to verify proper usage rules with C / JNI integration. JNI can be one complicated beast, and CBMC handily managed rule checks for its use. I'm an extremely careful developer who unit tests everything and strives for 99% coverage. CBMC was still able to detect a memory overwrite flaw in a networking library I wrote that was based on undefined behavior due to integer promotion and offset math. This passed the various sanitizers and unit tests I had in place, but CBMC was able to reduce it to an actual crash condition that was potentially exploitable. I don't think I can over-emphasize the usefulness of this tool.

nanolith 3y ago

Thanks. That is useful. I would suggest looking into CBMC and similar tools as well. Model checking is incredibly useful.

antonio2368 3y ago
Sadly I never put enough effort into trying out such checks. but your excitement about them gives me motivation to properly try them out.
- nanolith 3y ago
  CBMC is subtle and will require some code changes to use effectively. The real key for using it, in my opinion, is to isolate individual classes and functions. Avoid instrumenting code with recursion and loops, and focus on defining and verifying function contracts, class invariants, and resource / memory lifetimes. It will require a significant amount of work to mock up standard library and third party library APIs, but the real beauty of CBMC is that once you define the interface contracts for these APIs and libraries, you can verify every use of them. I used CBMC previously to verify proper usage rules with C / JNI integration. JNI can be one complicated beast, and CBMC handily managed rule checks for its use. I'm an extremely careful developer who unit tests everything and strives for 99% coverage. CBMC was still able to detect a memory overwrite flaw in a networking library I wrote that was based on undefined behavior due to integer promotion and offset math. This passed the various sanitizers and unit tests I had in place, but CBMC was able to reduce it to an actual crash condition that was potentially exploitable. I don't think I can over-emphasize the usefulness of this tool.