> My fuzzer finds that these 2 accesses can be executed concurrently The fuzzer is wrong. Have a look at the first assert() in lockBtree(), which checks the that sqlite3BtreeEnter() did lock correctly. > they are protected by different locks Do you have any evidence for this assertion? A BtShared object has a single Pager, which has a single Wal, which has a single file, which has a single unixShmNode.