FizzBee Test adaptor proof of concept

[jayaprabhakar]

This PR includes the Refinement mapping code required on Slate DB side to execute the tests. Refinement mapping just shows how the concrete implementation maps to the abstract model. It has two parts

• Mapping for actions: For example: how action Put in the model translates to db.PutWithOptions(...) in the Go code. This is actually trivial, and easily generated (ChatGPT got it correct with careful prompting and GitHub Copilot got it mostly correct without any prompting, but had to manually edit the code).
• Mapping for states: For example, How the DB's state or the ObjectStore with SSTs map to the Python dictionary in the model. This, at present, needs some careful thinking. I believe this could be simplified and improved to automate the code generation, I will work on it in parallel.

The test runner and the specific test cases are not included in this PR.

• Test Cases: The test cases are just data files generated when the fizzbee model checker is run. For the first model that is merged in the main slatedb repo, the data files are 100s of MB. So this must end up in some object store, and figure out how to make the workflow smooth.

• Test Runner: The test runner would be part of fizzbee, I will create a docker image.

  • At present, I have implemented only the tests for single threaded usage. For example Put(k1, v1), Get(k1, "committed"), Get(k1, "uncommitted"), Flush(), .... and so on one after another, and verify the states and the return values match what is expected based on the model. This is equivalent to most manually created tests. This covers only around 10% of the possible cases created by the FizzBee model.
  • Validating the concurrent behavior: This is the most interesting part and not currently testing in the slatedb-go implementation. For example, there is no test to ensure of Get(uncommitted) does not look at Immutable WALs. Because that will happen only if we have a way to pause a thread after freeze but before the immutable WALs are flushed. I will start with linearizability testing as it is easy to implement but resource intensive, but I actually want to implement a linear time atomicity testing but that's a bit complex though.

[criccomini]

Woah. Was this codegen'd from the fizzbee proof in the slatedb repo?

[jayaprabhakar]

Oops, I am writing a document and sharing the early draft to get some feedback. (Since I am mostly working alone and could easily be blinded by obvious issues and hidden complexities)

The PR includes the Refinement mapping code required on Slate DB side to execute the tests. Refinement mapping just shows how the concrete implementation maps to the abstract model. It has two parts

• Mapping for actions: For example: how action Put in the model translates to db.PutWithOptions(...) in the Go code. This is actually trivial, and easily generated (ChatGPT got it correct with careful prompting and GitHub Copilot got it mostly correct without any prompting, but had to manually edit the code).
• Mapping for states: For example, How the DB's state or the ObjectStore with SSTs map to the Python dictionary in the model. This, at present, needs some careful thinking. I believe this could be simplified and improved to automate the code generation, I will work on it in parallel.

The test runner and the specific test cases are not included in this PR.

• Test Cases: The test cases are just data files generated when the fizzbee model checker is run. For the first model that is merged in the main slatedb repo, the data files are 100s of MB. So this must end up in some object store, and figure out how to make the workflow smooth.

• Test Runner: The test runner would be part of fizzbee, I will create a docker image.

  • At present, I have implemented only the tests for single threaded usage. For example Put(k1, v1), Get(k1, "committed"), Get(k1, "uncommitted"), Flush(), .... and so on one after another, and verify the states and the return values match what is expected based on the model. This is equivalent to most manually created tests. This covers only around 10% of the possible cases created by the FizzBee model.
  • Validating the concurrent behavior: This is the most interesting part and not currently testing in the slatedb-go implementation. For example, there is no test to ensure of Get(uncommitted) does not look at Immutable WALs. Because that will happen only if we have a way to pause a thread after freeze but before the immutable WALs are flushed. I will start with linearizability testing as it is easy to implement but resource intensive, but I actually want to implement a linear time atomicity testing but that's a bit complex though.