Entremets

entremets是一种美味的甜点。字面上来说，它的意思是介于两餐之间。

另一方面，entremets是一个测试库，可以将SQL查询交织在一起。

目标

识别可序列化异常很困难。本项目旨在

• 提供一种简单的语言来转换生产代码
• 快速找到异常
• 测试解决方案

隔离级别很混乱

SQL引擎提供不同的隔离级别。它们可以被归类如下

[^1]: 可序列化是从事务中预期的直观隔离级别。但它的性能让它变得糟糕。

大多数应用程序使用 读取已提交 隔离级别。

丢失更新场景

考虑这个两个进程同时运行的场景。entremets中的代码是

init do
    `insert into users (id, age) values (1, 10)`
end

process do
    begin read_committed
    let t1_age := `select age from users where id = 1`
    `update users set age := $t1_age + 1 where id = 1`
    commit
end

process do
    begin read_committed
    let t2_age := `select age from users where id = 1`
    `update users set age := $t2_age * 2 where id = 1`
    commit
end

您期望当两个进程都完成时，select age from users where id = 1的结果是 21 或 22。

在entremets中，您可以通过向规范中添加此行来测试此属性

property eventually(`select age from users where id = 1` in {21, 22})

现在让我们在entremets下运行这个测试（mets是规范，entremets找到异常）

> entremets lost_update.mets
Following property was violated: eventually(`select age from users where id = 1` in {21, 22})
The following counter example was found:
...

输出显示了这个属性的反例。它显示了获得此状态的过程跟踪。

entremets的状态

目前entremets处于非常早期阶段。它仅支持读取已提交的隔离级别和非常有限的SQL语法。

请不要犹豫，为任何您觉得缺失的功能提交问题。