gitsync.py — multi-machine coordination for the verification campaign, over git.
The machines share nothing but the GitHub remote, so the remote is the lock.
Two operations matter:
claim(run_id) -- atomically take ownership of a run, or discover someone
else already has it
publish(...) -- record a finished run and push it, so every other machine
(and the user, from anywhere) sees the result immediately
WHY A SEPARATE WORKTREE. Every git operation here runs in a dedicated worktree
under `.sync/`, never in the checkout the solver is running from. This is not
tidiness. `run_ensemble.py` carries a 20-line comment about the day a
`git pull --rebase --autostash` replaced a results file underneath a running
worker: a file handle names an inode, not a path, so the worker kept happily
appending to an unlinked inode and 5 rows / 6.2 core-hours were written into
nothing for three hours before anyone noticed. A campaign that pulls and
pushes after every run would re-arm that trap on a much shorter fuse. Confining
git to a worktree the solver never reads means a pull cannot move anything the
solver is holding open.
WHY ONE FILE PER RUN. A claim is `claims/<run_id>.json`, written by exactly one
machine and never edited by another. Two machines therefore cannot produce a
CONTENT conflict -- only a push race, where the loser fetches, replays its one
commit on top and pushes again. That is a retry, not a merge. The alternative
(one shared ledger file appended by everyone) conflicts on every concurrent
finish and needs a real merge strategy.
The branch is separate from `main` so a day of automated commits does not land
in the history of the paper.
| str gitsync.machine_id |
( |
| ) |
|
Stable, UNIQUE identity for this host.
It was platform.node().split(".")[0], which is neither. This machine's
hostname changed from "MacBook-Pro" to "Mac.san.rr.com" mid-campaign (a
router handing out a domain), so it silently started claiming as "Mac" --
the id the OTHER machine already used. Two hosts sharing an id is not
cosmetic: claim() trusts pid liveness to tell a live sibling worker from a
dead one, and a pid is only meaningful on the machine that issued it. A
stale-looking claim could then be taken over while its real owner was still
computing, which is precisely the duplicate work the board exists to stop.
So the id is persisted on first use and never derived from a name that can
change underneath us. RADCLUSTER_MACHINE still overrides, for naming a
machine deliberately.
Definition at line 78 of file gitsync.py.
