4 ms·

Given that their entire code base is written in C++, and switching to a different language would be a significant retooling for the team, I think it's reasonabl

Given that their entire code base is written in C++, and switching to a different language would be a significant retooling for the team, I think it's reasonable to assume that it did not. Language choice is rarely made on the grounds of specific features, and is often made on the grounds of ergonomics and team knowledge. A more revealing question is, "How are you dealing with memory safety in this implementation?" There are ways to improve memory safety in C++ through tooling and idiomatic style. Are these things being used?

antonio2368 3y ago
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.

antonio2368 3y ago

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.