用约束阻止，只重试 40001

目标

重现“先检查再插入”的代码在两个会话中造成重复注册的情形，然后清理已有的重复，并用 UNIQUE 和 INSERT … ON CONFLICT 挡住。预订重叠用排除约束（EXCLUDE）解决，座位互换用 DEFERRABLE UNIQUE 解决。对跨越多行的规则，用 psycopg 3 写一个 SERIALIZABLE 重试循环来守护，最后整理每个不变量该放在哪里。

为什么重要

应用“先检查再写入”的规则，会在检查与写入之间的缝隙里被破坏，而这道缝隙只有在负载集中时才会暴露。数据库约束与隔离级别无关，始终成立，而且之后加入的代码也绕不过去。无法用约束来写的规则，就交给 SERIALIZABLE，但重试循环重试哪些错误、把哪些错误向上抛，决定着正确性。所以评分器不只看你写的文件，还会确认约束是否确实挂在系统目录上，并亲手插入反例行，然后回滚。重试循环则在故意制造错误的另一个数据库上调用来检验。

环境

PostgreSQL 16 已经在 Pod 内运行。连接方式是 psql -h 127.0.0.1 -U lab -d labdb，密码是 lab（export PGPASSWORD=lab）。工作文件全部放在 /root/svccs/invariants/。表都创建在 inv schema 下。Python 已经准备好 python3 和 psycopg 3。

步骤

创建并加载 /root/svccs/invariants/schema.sql。以 DROP SCHEMA IF EXISTS inv CASCADE; CREATE SCHEMA inv; 开头，创建下面的“表”并插入行。这一步除了表中写明的约束，不要加其他约束。
创建 /root/svccs/invariants/signup_naive.sql。在事务中统计 inv.signups_naive 里 race@example.com 有多少个（\gset），用 pg_sleep(2) 停顿之后，只在为 0 时才插入。让两个会话重叠运行，制造重复，并把该邮箱的行数以 rows <수>（占位符为行数）写入 /root/svccs/invariants/02-race.txt。
清理 inv.members 中已有的重复（保留最小的 id），并以 members_email_key 为名加上 UNIQUE (email)（不可延迟）。在 /root/svccs/invariants/signup.sql 中，用使用 psql 变量 :'email' 的一条语句（没有 BEGIN/COMMIT）写出 ON CONFLICT (email) DO NOTHING RETURNING id 的注册。用 race@example.com 让两个会话重叠运行，并在 /root/svccs/invariants/03-unique.txt 中逐行写入 returned_a、returned_b（每个会话收到的行数）、rows（该邮箱的行数）。
在 /root/svccs/invariants/touch.sql 中用一条语句写 upsert。不存在就插入（visits 为 1），存在就在现有 visits 上加 1，无论哪种，都用 RETURNING id, visits 返回该行。把对已存在的 kim@example.com 分别运行 signup.sql 和 touch.sql（之后回滚）时收到的行数，以 do_nothing_rows <수>、do_update_rows <수>（占位符均为行数）写入 /root/svccs/invariants/04-upsert.txt。
创建 btree_gist 扩展，并统计同一房间里 [) 范围重叠的已有预订的对数。在重叠的对中，把 id 较大的一方改成 status = 'cancelled'（不删除），并以 bookings_no_overlap 为名，创建只对活动（status = 'active'）预订加的排除约束——房间相同且 tstzrange(starts_at, ends_at, '[)') 重叠的不被允许。在 /root/svccs/invariants/05-exclude.txt 中写入 overlaps_found <센 쌍 수>、cancelled <취소 상태 행 수>、sqlstate <겹치는 예약을 넣었을 때 받은 코드>（占位符依次为统计到的对数、已取消状态的行数、插入重叠预订时收到的代码）。
在 /root/svccs/invariants/swap.sql 中写两个 UPDATE，在一个事务里把 kim 的座位换成 14、lee 的座位换成 12。把用现在的 seats_seat_no_key 运行时收到的 SQLSTATE，以 immediate_error <코드>（占位符为代码）写入 /root/svccs/invariants/06-swap.txt，然后把同名约束以 DEFERRABLE INITIALLY DEFERRED 重新创建，再运行 swap.sql，真正完成互换。
在 /root/svccs/invariants/retry.py 中编写 withdraw(conninfo, wallet_id, amount, max_attempts=8)。规则完全按下面的“取款规则”。在同一个文件的 if __name__ == "__main__": 中，把 kim 家的两个钱包恢复为 100，让 6 个线程同时（对齐起点）在钱包 1、2 上轮流各取款 80，然后在 /root/svccs/invariants/07-retry.json 中写入 workers、committed、rejected、retries（全部尝试数 − 线程数）、final_sum（kim 家的合计）。
在 /root/svccs/invariants/map.json 中，对下面六个不变量的每一个，写入 {"where": "constraint" | "isolation" | "application", "how": "쓴 도구 한 줄"}（占位符为所用工具的一句话说明）。评分器还会检查写成 constraint 的那些，当前数据库里是否确实挂着。

表

inv.members        id bigserial PK, email text NOT NULL, visits int NOT NULL DEFAULT 1
                   행: kim@example.com, lee@example.com, legacy@example.com, legacy@example.com
inv.signups_naive  id bigserial PK, email text NOT NULL                (행 없음, 끝까지 제약 없음)
inv.bookings       id bigserial PK, room text, starts_at timestamptz, ends_at timestamptz, who text,
                   status text NOT NULL DEFAULT 'active',
                   CONSTRAINT bookings_positive_length CHECK (starts_at < ends_at)
                   행: river 10:00~11:00 kim · river 11:00~12:00 lee · river 11:30~12:30 park
                       · hill 10:00~11:00 choi   (모두 2026-10-01, 시간대 +09)
inv.seats          id int PK, passenger text NOT NULL, seat_no int NOT NULL,
                   CONSTRAINT seats_seat_no_key UNIQUE (seat_no)
                   행: (1, kim, 12) (2, lee, 14) (3, park, 15) (4, choi, 16)
inv.wallets        id int PK, family text, owner text, balance int   (모두 NOT NULL)
                   행: (1, kim, kim-a, 100) (2, kim, kim-b, 100) (3, lee, lee-a, 50) (4, lee, lee-b, 50)

取款规则

연결은 conninfo 로 새로 연다. 격리 수준은 SERIALIZABLE.
한 트랜잭션: wallet_id 의 family 를 읽고 → 그 family 의 balance 합계를 읽고 →
  합계 < amount 면 아무것도 바꾸지 않고 {"status": "rejected", "attempts": n} 을 돌려준다
  아니면 UPDATE inv.wallets SET balance = balance - amount WHERE id = wallet_id 후 커밋하고
  {"status": "committed", "attempts": n} 을 돌려준다     (n = 이번 호출에서 시도한 횟수)
SQLSTATE 40001·40P01 이면 트랜잭션 전체를 처음부터 다시 한다(짧은 무작위 대기, 합계 1초 이내).
그 밖의 오류는 다시 하지 않고 그대로 올려보낸다. max_attempts 번 모두 실패하면 마지막 오류를 올려보낸다.

六个不变量（第 8 步）

member_email_unique       이메일 하나에 회원 하나
room_no_overlap           같은 방의 활성 예약 시간이 겹치지 않는다
seat_unique               좌석 하나에 승객 하나(맞바꾸는 동안은 잠깐 깨져도 된다)
booking_positive_length   예약은 끝이 시작보다 뒤다
family_sum_nonnegative    가족 지갑 합계가 음수가 되지 않는다(여러 행에 걸친 조건)
welcome_mail_once         가입 환영 메일(외부 메일 서비스 호출)은 한 번만 보낸다

参考

psql 用 -v email=값（占位符为值）传递变量，在文件中以 :'email' 使用。像 -c "BEGIN" -f 파일 -c "COMMIT"（占位符为文件）这样给出多个，就会在一个会话中依次运行。想在错误中看到 SQLSTATE，请加上 -v VERBOSITY=verbose。
要让两个会话重叠，就把一个用 & 放到后台，稍等片刻再运行另一个，然后 wait。
常见错误：没有 UNIQUE，只用 WHERE NOT EXISTS 之类的应用层检查；把范围写成 []，连相接的预订也挡住了；用临时编号绕过互换，约束却原封不动；重试循环用 except Exception 把约束违反也重做，或者把失败报告成成功。
产出和数据库会在会话结束后消失。需要的话请另行保存。

创建没有约束的表

创建并加载 /root/svccs/invariants/schema.sql——在 inv schema 中，完全按说明中的“表”创建 members、signups_naive、bookings、seats、wallets。

如果以 DROP SCHEMA IF EXISTS inv CASCADE 开头，无论重新加载多少次，状态都相同。psql 即使出错也会继续运行下一条语句，所以请加上 -v ON_ERROR_STOP=1。时间要像 '2026-10-01 10:00+09' 那样写到时区。

“先检查再插入”造成了重复

用 /root/svccs/invariants/signup_naive.sql 让两个会话重叠，在 inv.signups_naive 中制造 race@example.com 的重复，并把行数以 rows <行数> 写入 /root/svccs/invariants/02-race.txt。

把用 SELECT count(*) AS n … \gset 数出的值以 :n 使用。两个会话都必须在对方提交之前就数完，才会都看到 0——把一个用 & 放到后台，0.5 秒后再运行另一个。如果依次运行，第二个会看到 1，就不会插入。

UNIQUE 与 ON CONFLICT DO NOTHING

清理 inv.members 中的重复并加上 members_email_key UNIQUE (email)，然后用 /root/svccs/invariants/signup.sql（一条语句）让两个会话重叠，把 returned_a、returned_b、rows 写入 /root/svccs/invariants/03-unique.txt。评分器会用探测用邮箱把 signup.sql 运行两次，然后回滚。

约束也会检查已有的行，所以如果 legacy 重复还在，ALTER TABLE 会失败。用 DELETE … USING 把相同邮箱中 id 较大的删掉。重叠的两个会话中，后一个会话会等前一个会话提交，然后什么都不插入，RETURNING 也是空的。

DO UPDATE 与 RETURNING 的区别

在 /root/svccs/invariants/touch.sql 中用一条语句写出增加 visits 的 upsert，并把 signup.sql、touch.sql 对已有会员返回的行数写入 /root/svccs/invariants/04-upsert.txt。评分器会用探测用邮箱把 touch.sql 运行三次，查看 id 和 visits。

在 SET 子句里，现有行用表别名（AS m）指代，想插入的行用 EXCLUDED 指代。EXCLUDED.visits 是默认值 1，在它上面加，无论运行多少次都是 2。DO NOTHING 的 RETURNING 不会返回被跳过的行。

预订重叠交给 EXCLUDE

创建 btree_gist，统计已有重叠并取消，然后创建只对活动预订加的 bookings_no_overlap 排除约束，并把 overlaps_found、cancelled、sqlstate 写入 /root/svccs/invariants/05-exclude.txt。评分器会向探测用房间插入重叠的、相接的、已取消的预订来检验，然后回滚。

重叠用 tstzrange(starts_at, ends_at, '[)') && … 来判断。在 '[)' 下，11 点结束的预订与 11 点开始的预订不重叠——如果用 '[]'，由于 kim、lee 的预订，约束本身就加不上。部分约束是 EXCLUDE … WHERE (status = 'active')。

座位互换与 DEFERRABLE

用 /root/svccs/invariants/swap.sql，把在立即检查的 UNIQUE 下收到的错误以 immediate_error 写入 /root/svccs/invariants/06-swap.txt，再把 seats_seat_no_key 以 DEFERRABLE INITIALLY DEFERRED 重新创建，然后把 kim 换成 14、lee 换成 12。评分器会查看约束属性，在事务内检验互换和重复，然后回滚。

ALTER CONSTRAINT 只能修改外键，所以在同一条 ALTER TABLE 里同时使用 DROP CONSTRAINT 和 ADD CONSTRAINT。在立即检查下，第一条 UPDATE 结束的瞬间就有了两个 12，从而报 23505。用临时编号（0）换三次虽然能通过，但约束仍然是立即检查。

只重试 40001 的重试循环

在 /root/svccs/invariants/retry.py 中按取款规则编写 withdraw，并把用 6 个线程同时取款的结果写入 /root/svccs/invariants/07-retry.json。评分器会在单独的数据库上故意触发 40001、40P01、23514，同时调用 withdraw。

用 psycopg.connect(conninfo, autocommit=True) 打开，设置 conn.isolation_level = psycopg.IsolationLevel.SERIALIZABLE，然后在循环里打开 with conn.transaction(): 块。请根据异常的 sqlstate 来分支——如果用 except Exception 全部重做，连约束违反也会被重复。读取合计的 SELECT 也必须放在循环里，这样重做时才会看到新值。

每个不变量该放在哪里

在 /root/svccs/invariants/map.json 中，为六个不变量各自写入 where（constraint、isolation、application）和 how。评分器会检查写成 constraint 的，当前数据库里是否确实挂着，并且是否真的拒绝反例。

CHECK 看不到正在检查的行之外的其他行，所以多行的合计无法用约束来写。事务即使回滚，已经发出去的外部调用也收不回来，所以那是数据库无法守护的规则。