3 ms·

The issue is that the race condition exists in the database, not in any application code. So you can either simulate the race, or you need to integration test,

The issue is that the race condition exists in the database, not in any application code. So you can either simulate the race, or you need to integration test, and that's outside the scope of TLA+ and model checking. I haven't heard of Coyote (it's still amazing how many tools are out there). It's good that it operates on the actual code level, but I'm still not sure that would reproduce concurrency non-determinism at the database level.

skyde 3y ago
yes if your test are using a mock of the db ex: https://github.com/microsoft/coyote/blob/main/Samples/AccountManager/AccountManager/InMemoryDbCollection.cs https://github.com/microsoft/coyote/blob/main/Samples/Accoun... you can simulate the races. The problem is your mock need to implement the same isolation level as your real DB and support transaction ... You could use SQLITE in memory DB to run your test but that would make your test a lot slower I assume.
- amw-zero 3y ago
  Exactly, it's a tricky problem. Implementing all transaction isolation levels in a mock is quite an ambitious endeavor.
- sophiabits 3y ago
  The problem is that you don’t really know if your mock accurately implements the behavior of the database. The only way you could verify the mock behaves correctly would be to run the mock and a real database instance through a set of tests to verify they both implement different isolation levels identically. At that point—why bother with the mock at all? Cutting out the intermediary and running integration tests of your application against a real database will be faster. You can’t use SQLite here either because all SQLite isolation levels are serializable anyway, which is _very_ different from how PostgreSQL works. Testing against SQLite could end up giving you a false sense of security that your code is safe against race conditions, whereas in reality it’s vulnerable when connected to a PostgreSQL server because of the difference in default isolation levels At this level of testing detail the only real option is to test against a real database that matches what you’re running in production. Otherwise you’re just testing a mock.
  - skyde 3y ago
    I didn't know that Thanks for your comment. Except in the case of shared cache database connections with PRAGMA read_uncommitted turned on, all transactions in SQLite show "serializable" isolation

skyde 3y ago

yes if your test are using a mock of the db ex: https://github.com/microsoft/coyote/blob/main/Samples/AccountManager/AccountManager/InMemoryDbCollection.cs https://github.com/microsoft/coyote/blob/main/Samples/Accoun... you can simulate the races. The problem is your mock need to implement the same isolation level as your real DB and support transaction ... You could use SQLITE in memory DB to run your test but that would make your test a lot slower I assume.

amw-zero 3y ago
Exactly, it's a tricky problem. Implementing all transaction isolation levels in a mock is quite an ambitious endeavor.
sophiabits 3y ago
The problem is that you don’t really know if your mock accurately implements the behavior of the database. The only way you could verify the mock behaves correctly would be to run the mock and a real database instance through a set of tests to verify they both implement different isolation levels identically. At that point—why bother with the mock at all? Cutting out the intermediary and running integration tests of your application against a real database will be faster. You can’t use SQLite here either because all SQLite isolation levels are serializable anyway, which is _very_ different from how PostgreSQL works. Testing against SQLite could end up giving you a false sense of security that your code is safe against race conditions, whereas in reality it’s vulnerable when connected to a PostgreSQL server because of the difference in default isolation levels At this level of testing detail the only real option is to test against a real database that matches what you’re running in production. Otherwise you’re just testing a mock.
- skyde 3y ago
  I didn't know that Thanks for your comment. Except in the case of shared cache database connections with PRAGMA read_uncommitted turned on, all transactions in SQLite show "serializable" isolation