디자인 리스 검증은(는) 무엇을 하나요?

crates/server/tla/DesignLeases.tla는 하나의 저장소를 공유하는 두 Finite 서버와 그 사이를 이동하는 디자인 하나에 대한 TLA+ 모델입니다. TLC(TLA+ 모델 검사기)는 작은 범위 내에서 모든 가능한 단계 순서를 시도하고 두 가지 규칙을 검사합니다.

StoredEditsStay (펜싱): 저장소가 편집을 수락하면, 다른 서버에 있는 오래된 복사본이 이를 덮어쓸 수 없습니다. 이 규칙이 깨지면, 중단되었던 서버가 깨어나서 새 소유자가 저장한 편집을 지워버립니다.
AckedEditsStay: MCP 도구가 완료되었다고 보고한 편집은 저장소에 있거나, 저장할 수 있는 복사본에 있어야 합니다. 단, 편집이 저장되기 전에 서버가 충돌하거나 리스가 만료된 경우는 제외합니다. 이 규칙이 깨지면, 에이전트는 편집이 성공했다는 응답을 받았지만 실제로 편집은 사라집니다. 뷰어는 편집이 사라진 것을 보게 되고, 에이전트는 이에 대한 알림을 받지 못합니다.

현재 코드는 첫 번째 규칙을 통과하고 두 번째 규칙은 네 가지 알려진 방식으로 위반합니다. 이는 아래 "알려진 발견 사항"에 나열되어 있습니다.

변경 사항이 관련 있나요?

예. 다음 테이블의 어떤 함수를 변경한다면 관련 있습니다. 각 모델 단계는 해당하는 코드의 이름을 가지며, 리뷰어는 두 가지를 나란히 열어볼 수 있습니다.

모델 단계	코드
`CallStarts`, `CallFindsHandle`, `CallLoads`, `CallEdits`, `CallReads`	`mcp/mod.rs` `design`, `edit_checked`; `api.rs` `open`; `hub/mod.rs` `Hub::open`, `handle_for`; `hub/design.rs` `DesignHandle::load`, `edit`
`SaveTakes`, `SaveWrites`, `SaveFenced`, `SaveFails`, `SaveReleases`, `SaveDrops`	`hub/mod.rs` `persist`; `hub/design.rs` `take_save`, `save_failed`
`Unload`	`hub/mod.rs` `Hub::sweep`; `hub/design.rs` `unload_if_idle`, `is_idle`
`TickRenews` … `TickDiscovers`	`hub/mod.rs` `Hub::tick`, `let_go`, `remove`, `drop_copy`, `discover`, `summaries`; `hub/design.rs` `retire`, `end`, `lease`
`Owns`, `LeaseLapses`, `HeartbeatExpires`	`cluster.rs` `Members::now`, `lapsed`, `renewed`, `Cluster::owns`, `owner`
`CanClaim`, `Claimed`, 저장소 쓰기	`postgres/mod.rs` `claim`, `save`, `append`, `release`, `held`; `store.rs` `trait Store` (인메모리 공유 저장소도 일치해야 함)
`Start`, `Crash`	`hub/mod.rs` `Hub::shared`

경로는 crates/server/src/ 아래에 있습니다.

동기화 커밋: 6606714. 이것은 모델이 이 코드에 대해 마지막으로 검증된 커밋입니다. 이후에 해당 코드 영역에서 변경된 사항을 보려면 다음 명령을 실행하세요:

git diff 6606714 -- crates/server/src/hub crates/server/src/mcp/mod.rs crates/server/src/api.rs crates/server/src/cluster.rs crates/server/src/postgres/mod.rs crates/server/src/store.rs

diff가 테이블의 함수를 건드린다면, 통과를 신뢰하기 전에 해당하는 모델 단계를 다시 읽으세요. 변경된 각 단계가 새 커밋에서의 코드와 여전히 일치함을 확인한 후에만 이 파일의 동기화 커밋을 앞으로 이동하세요.

실행하기

crates/server/tla/check.sh          # 일상적인 검사, 약 2분
crates/server/tla/check.sh --full   # Finding4.cfg와 AllFixes.cfg 추가, 약 3분 더 소요

스크립트는 첫 실행 시 TLC(tla2tools.jar v1.7.4, SHA-256 검증)를 ~/.cache/finite에 다운로드합니다. Java 11 이상이 필요합니다. 각 설정은 현재 코드에 대해 기록된 결과를 제공할 때 ok를 출력하고, 그렇지 않으면 FAIL을 출력합니다. 규칙이 깨지면, 최단 경로와 함께 TLC의 출력이 crates/server/tla/<설정>.out에 저장됩니다. Git은 이러한 파일을 무시합니다.

설정	적용된 수정 사항	범위	현재 결과
`Fencing.cfg`	없음	편집 1회, 읽기 1회, 핸들 2개, 최대 18단계의 모든 동작	통과, 약 280만 상태, 2분
`DesignLeases.cfg`	없음	편집 1회, 핸들 2개	발견 1, 몇 초
`Finding2.cfg`	FixRetire	편집 1회, 핸들 2개	발견 2
`Finding3.cfg`	FixRetire, FixOrphan	편집 2회, 핸들 2개	발견 3
`Finding4.cfg`	+ FixStaleDrop	편집 2회, 핸들 2개	발견 4, 약 1분
`AllFixes.cfg`	네 가지 모두	편집 2회, 핸들 2개	통과, 약 1600만 상태, 2분

모든 설정은 저장소의 에포크를 3으로 제한하며, 충돌이나 실패한 쓰기는 포함하지 않습니다. 읽기는 MCP 읽기 도구나 뷰어의 소켓처럼 디자인을 편집하지 않고 로드하는 호출입니다. 펜싱에는 읽기가 하나 필요합니다. 오래된 복사본이 존재하려면 두 호출이 디자인을 로드했어야 하기 때문입니다. 읽기를 포함한 전체 상태 공간은 30분 안에 끝나지 않았기 때문에, check.sh는 TLC의 반복 심화(-dfid 18)를 사용하여 실행합니다: 최대 18단계의 모든 동작. 가장 짧은 오래된 덮어쓰기는 17단계가 소요됩니다. 발견 설정은 범위 내의 모든 것을 탐색합니다. TLC는 첫 번째 위반된 규칙에서 멈추므로, 각 발견 설정은 이전 발견에 대한 제안된 수정 사항을 켜놓습니다. Fix* 상수는 가상 시나리오 스위치입니다. 모두 FALSE이면, 모델은 현재 코드와 동일합니다.

결과 읽기

/statechart 스킬과 함께 각 결과를 읽으세요. 이 스킬은 TLC의 위반된 규칙까지의 최단 경로를 일반 언어로 된 번호 매기기 단계 목록으로 바꾸고, 설정이 통과하면 디자인이 서버 간에 어떻게 이동하는지 차트를 그립니다.

설정이 FAIL을 출력하면, 버그가 코드에 있는지 모델에 있는지 결정하세요:

실제 버그는 코드에서 재현할 수 있는 경로를 제공합니다. 각 단계를 따라가며, 테이블의 함수를 열고, 코드가 해당 순서로 그 단계를 허용하는지 확인하세요. 그런 다음 아래의 발견 사항처럼 코드의 언어로 경로를 보고하세요. 검사가 통과할 때까지 규칙이나 범위를 약화시키지 말고, 요청받지 않는 한 제품 코드를 변경하지 마세요.
모델링 오류는 코드가 실행할 수 없는 단계를 제공합니다. 예: 코드가 하나의 잠금(상태 뮤텍스, 지속성 뮤텍스) 아래에서 실행하는 두 단계가 모델에서 분리된 경우; 코드에 있는 가드가 없는 모델 단계; 갱신 직후에 만료되는 하트비트 등. 코드와 일치하도록 모델을 수정하고, 무엇을 수정했는지 명시하세요.
Fencing.cfg 위반은 깊이 제한 실행에서 발생하며, 해당 경로는 단계 이름을 지정하지 않습니다. 명명된 최단 경로를 얻으려면 동일한 설정을 너비 우선으로 실행하세요: cd crates/server/tla && java -cp ~/.cache/finite/tla2tools-1.7.4.jar tlc2.TLC -workers auto -config Fencing.cfg DesignLeases.tla. 가장 첫 번째 위반에서 멈추며, "의도적으로 해당 코드를 변경할 때" 아래의 위반에 대해 약 6초가 소요됩니다.
**error**는 TLC가 완료되지 않았음을 의미합니다: 구문 오류, 또는 액션이 할당되지 않은 변수를 남긴 경우. .out 파일을 읽으세요.

FAIL이지만 코드가 이전에 규칙을 위반했고 지금은 통과하는 것은 좋은 소식입니다. "알려진 발견 사항" 아래의 발견 테이블은 이를 기록하는 방법을 보여줍니다.

의도적으로 해당 코드를 변경할 때

코드와 같은 커밋에서 모델 단계를 변경하고, 함수 이름을 명시하는 주석을 유지하세요.
변경으로 발견 사항이 수정되면, 수정 사항을 스위치가 아닌 코드로 모델에 넣으세요: Fix* 상수를 삭제하고, 단계가 새 코드처럼 동작하도록 만들고, 모든 설정에서 해당 스위치를 제거하세요. 다음 발견 사항의 설정이 기본 설정이 되고, check.sh는 새로운 예상 결과를 가져옵니다.
통과를 신뢰하기 전에, 의도적으로 코드를 깨뜨린 스크래치 복사본을 만들고, 모델에서도 깨뜨림을 반영한 후, 설정이 이를 잡아내는지 확인하세요. 예를 들어, PgStore::save에서 AND epoch = $3을 빼고 SaveWrites에서 x.ptok = store.epoch를 빼면, Fencing.cfg는 StoredEditsStay를 위반합니다. 결코 실패하는 것을 본 적이 없는 검사는 아무것도 증명하지 못합니다.
check.sh --full을 실행한 다음, 동기화 커밋을 앞으로 이동하세요.

알려진 발견 사항

각각은 6606714 커밋의 코드에 대한 경쟁 조건입니다. 각각에서 에이전트의 도구 호출은 성공을 반환하지만 편집은 사라집니다.

편집이 이미 마지막 스냅샷을 저장 중인 복사본에 도착합니다. 서버 A가 디자인을 로드했고, MCP 호출이 Hub::open을 통과했습니다. 서버 B가 합류하여 디자인을 획득합니다(A의 리스 만료도 동일하게 작용합니다). A의 틱은 let_go를 호출하고, retire는 복사본을 Retiring으로 표시합니다. 저장 작업의 take_save는 마지막 스냅샷을 가져옵니다. 그런 다음 호출의 DesignHandle::edit가 잠금을 획득하고 retiring 중인 복사본에 커밋합니다. edit는 life를 전혀 확인하지 않기 때문입니다. 저장 작업은 편집 없이 스냅샷을 저장하고, 리스를 해제하며, drop_copy는 pending을 지웁니다. B는 편집 없이 디자인을 로드합니다. 실제 앱에서 이를 트리거하려면, 틱이 실행될 때 이미 여러 에이전트가 큰 write_html 호출을 실행하는 등 디자인의 잠금을 기다리는 편집이 있어야 합니다. 실행 취소, 다시 실행, 가져오기 및 댓글 업데이트도 동일한 경로를 사용합니다.
편집이 허브가 이미 목록에서 제거한 핸들에 도착합니다. 호출의 handle_for는 로드되지 않은 핸들을 반환합니다. B가 합류하고, A의 let_go는 로드된 것이 없음을 확인하므로 remove를 호출합니다. 호출의 load는 리스를 획득하고 해당 핸들에 복사본을 로드합니다. 다음 틱의 loaded 목록은 더 이상 이 핸들을 포함하지 않는 허브 목록에서 가져옵니다. 따라서 틱은 리스를 해제하고, 복사본의 다음 저장은 Fenced로 실패합니다. 이는 중단이 필요 없으며, 서버가 합류하기만 하면 됩니다.
틱이 읽은 후 다시 로드된 복사본을 삭제합니다. 하나의 서버, 멤버십 변경 없음. 틱이 lease()(토큰 1)를 읽습니다. 그런 다음 디자인이 언로드되고, 호출이 다시 로드(토큰 2)하여 편집을 커밋합니다. 틱이 held()(토큰 2)를 읽고, 2 ≠ 1임을 확인한 후 drop_copy를 호출합니다. drop_copy는 대기 중인 편집을 포함하여 새 복사본을 종료합니다. 윈도우는 두 읽기 사이이므로 좁지만, 모든 틱에서 실행됩니다.
방금 리스를 갱신한 서버가 오래된 복사본을 제공합니다. B가 리스를 초과하여 중단되고, A가 디자인을 인수하여 편집을 저장합니다. B가 깨어납니다. B의 틱은 하트비트를 갱신하고, 그 순간부터 Members::now는 B를 살아있고 다시 소유자로 간주합니다. 그러나 let_go 루프는 아직 실행되지 않았습니다. B에 대한 호출이 여전히 Live인 오래된 복사본을 로드하고 편집을 커밋하며, 이는 나중에 Fenced로 실패합니다. 이를 위해서는 먼저 중단이 필요합니다.

AllFixes.cfg는 각 발견 사항에 대해 하나의 제안된 수정 사항을 검사합니다: edit는 Live가 아닌(1) 또는 목록에 없는(2) 복사본을 거부합니다. 틱은 자신이 읽은 토큰과 일치하는 경우에만 복사본을 삭제합니다(3). 만료 후 갱신된 서버는 놓을 때까지 자신을 제외합니다(4). 네 가지 모두가 적용되면 AckedEditsStay는 이러한 범위에서 유지됩니다.

포함되지 않는 것

하나의 디자인, 두 서버, MCP 편집. 실행 취소, 다시 실행, 가져오기, 댓글 및 이름 변경은 동일한 잠금 및 커밋 경로를 사용하지만 별도로 모델링되지는 않았습니다. Hub::delete도 마찬가지입니다.
파일 저장소 및 FINITE_NODES 핸드오프(hand_off_one, adopt), 라우터.
종료 시 Hub::flush, 저널 압축 임계값(COMPACT_AFTER, COMPACT_BYTES), 뷰어 재개를 위한 버퍼인 Recent.
타이밍. TLC는 모든 단계 순서를 시도하므로, 모델은 경쟁 조건이 존재함을 보여주지 얼마나 자주 발생하는지는 보여주지 않습니다. 서버 자체 리스 타이머(Members::lapsed)가 데이터베이스가 하트비트를 만료된 것으로 간주하는 것보다 늦어지지 않는다고 가정합니다. 이는 두 클록이 동일한 속도로 실행될 때 유지됩니다.
더 큰 범위. 더 많은 편집, 읽기, 핸들 또는 에포크, 충돌 및 실패한 쓰기는 일상적인 설정에 포함되지 않습니다. AllFixes.cfg는 편집 1회, 충돌 1회, 실패한 쓰기 1회(340만 상태)로도 통과했습니다. 18단계를 초과하는 펜싱은 아직 완료되지 않았습니다: 편집 1회와 읽기 1회로 5000만 개의 고유 상태를 통과했지만 여전히 진행 중이었습니다. 읽기 없는 오래된 펜싱 통과를 신뢰하지 마세요: 편집 하나만으로는 하나의 복사본만 로드되므로 아무것도 오래될 수 없습니다.

디자인 리스 검증