Tine's storage layer now has a formally proved model

[martinkoutecky]

I wrote the outline of this post and asked Claude (Opus 5.5) to expand, polish, and fill in details. I'm sure Claude will be happy to answer any follow-up technical questions that I may not be able to answer; I'm trying to keep the post itself short-ish, but I think there is a lot of interesting stuff to be learned so ask away.

TL;DR. Tine's save engine now follows a written specification with a precise guarantee: under clearly stated assumptions, text Tine has told you is saved is never lost to a crash, a power cut, or a race with another program or window. That guarantee is checked by a model checker and mathematically proved in the Lean proof assistant, for graphs of any size. As far as I know, this level of rigor has so far been the domain of large companies like AWS and of research projects, not of hobby-scale apps; AI models are what made it feasible here. The code is tested against the model, not proved. It shipped in 0.8 Beta, it is the foundation for the new command line, and performance is the same or better except for large renames.

Storage is a key layer for Tine, for two reasons: it has a lot to do with making Tine fast, and it has to be solid, because Tine writes your real notes and every bug there is a potential data-loss incident.

As far as reports go, data safety has not been a big concern. But watching Claude work on storage fixes, I saw a pattern: make a fix, review it, find a race condition or another bug, fix that, find another race... Each fix took a long time to converge, and I could never be sure it had.

It was also never quite clear under what assumptions we were working, and what guarantees we wanted to get out of it. "Don't lose data" is not a specification.

So I decided we should have a written storage specification that is simple enough to reason about (at least for models), and that says clearly:

• what bad things can happen and must be survived: the app crashing, a power cut, a disk error, a sync tool or another editor changing files under Tine, several windows or the command line editing the same graph;
• where all bets are off: e.g. a malicious actor on your device, or a filesystem that claims to have saved data when it hasn't;
• and what Tine guarantees under those assumptions.

Fine: Claude wrote a spec, GPT (Sol) reviewed it and found bugs, Claude fixed them, Sol found more bugs... At some point I realized this process would probably not converge either. I remembered (partly from my training) that there is such a thing as model checking, and that those techniques might be relevant.

There was also a concrete reason this couldn't wait: the command line (tine CLI; its first, read-only version is in 0.8 Beta on Linux and macOS). Until now, each editing window held its page's unsaved text and saved it itself, with the logic split between the frontend and the Rust backend. A CLI that edits pages while the app is open would have been one more independent writer racing the windows, exactly the kind of situation where the fix-review-find-another-race loop never ends. The new design has one owner per graph: a backend "page host" that holds every page's text and does all the file I/O. App windows and the CLI are both just clients that send it text plus the version it was based on. That is what already lets the CLI read your open, unsaved edits, and what will let its editing commands (next) write pages safely while you are typing in the app. But it moves the whole save path into a new place, so we wanted to know precisely what it guarantees before building the CLI on top of it.

How it went

Week one (Sept 30 – Oct 3): spec first, then check it. Claude translated the English spec into Quint, an executable specification language built on TLA+, and checked it with random simulation and the TLC model checker. The checker kept finding executions where it was unclear whether anything had been "lost". Each one needed a ruling from me, which showed that the spec didn't actually define loss. We wrote that definition down; the next round still found six cases it didn't decide. After more than twenty rounds I stopped that approach.

Model first (Oct 3–4). We turned it around: the Quint model is the spec, and the English text only explains it. Two independent attempts (one by Claude, one by GPT) were merged into one model. This immediately found real design bugs that the English drafts also had. For example, a crash could make Tine forget that a save had not been confirmed, and a later discard of that page then lost the text on a power cut.

Exhaustive checking (Oct 4–8). TLC explores every possible interleaving of user actions, saves, crashes, power cuts and external writes, up to a size limit. This is compute-hungry: the state space explodes quickly, so the runs were spread over several machines for days. One complete run checked more than 4 billion steps between some 2 million distinct states, without a violation. Along the way it and the accompanying proofs found several more real defects, including typing during a discard and a launch step that trusted a file rename which might not survive a power cut. Final reviews of the model by two other models (GPT and Claude Fable) found two more, both fixed.

From "small graphs" to "every graph" (Oct 8–9). Model checking only covers bounded sizes. To go beyond that, the model was transcribed into the Lean proof assistant, and the whole guarantee was proved there in six rounds: for any number of pages, any number of edits, and every race scenario we model. Each round's proof was rebuilt and checked by an independent verifier agent. As a cross-check, the Lean and Quint versions were run side by side on every test scenario and agree on all 2,024 outcomes.

Rename and delete (Oct 9). Page rename (with rewriting every reference) and page delete were then added to the model. Lean proved that the extended model behaves exactly like the old one on everything that isn't a rename or delete. Its first attempt at the full guarantee failed, on a real hole that 120 hand-written scenarios and random simulation had all missed: you have unsent typing on a page, the command line deletes or renames that page, and your late typing silently overwrote the deletion. That case now comes back to you as a visible conflict. The fixed model was proved in full the same day.

Since then (Oct 10–14). The model kept growing as implementation needs came up: a fixed order for the steps of a rename (so that while Tine runs, the old page is only removed after the new page and every rewritten link are safely on disk), one general "operation" step that later features reuse, and a check that a new page can't take a name another file already claims. Each was added as an extension that leaves everything else unchanged, and each passes the full scenario set, every deliberately broken variant, and random simulation. The Lean proof caught up with them: the full no-loss guarantee, including renames and the new operation step, is proved for every reachable state, and so are the rename order, the name check and "deleted text always ends up in the trash". The proof work also found a spot where the model was sloppier than the code (cancelling a rename could reload a page that had already been closed); the model was corrected to match what the code already did. The last piece, that while Tine runs a renamed page always has a file at its old or its new path, is proved too (a crash or another program writing to one of those paths ends that promise; the no-loss guarantee still covers your text). Every property the model states is now proved for every graph size.

What is proved

Fast forward: we now have an English spec, a Quint model of it, and a formal proof that, under the stated assumptions, the current model gives these guarantees:

• No loss: the newest text Tine has acknowledged (saved, or kept as a recoverable draft) survives any crash, power cut or graph switch: it is either in its file or restored on the next launch.
• No silent replacement: background activity never replaces text you haven't saved yet.
• No blind overwrite: a Tine save only replaces the exact file contents it checked were there, and never contents you were never shown.
• Every page Tine changes on your behalf (a rename rewriting references, a delete) is covered by the same rules.

The proof is equally clear about what is not covered, and these are written down as accepted, not as losses:

• text Tine never acknowledged (e.g. what you typed in the last fraction of a second before the app crashed);
• another program writing a file in the tiny window between Tine's check and its save. No portable OS mechanism closes this window; every app that saves files has it;
• a filesystem or sync provider that loses data it confirmed as written;
• after an interrupted move between pages, the moved text can end up in both places: duplicated, never lost.

As far as I know, this kind of work has so far been done mostly in large-scale industry: AWS has used TLA+ on its core services for over a decade, and Microsoft and MongoDB do similar things. Most of those check the model up to some size; here the guarantee is proved for graphs of any size. Academia goes further still: projects like FSCQ, a verified file system, prove that the code itself is correct, which we don't (see below). But I don't know of a hobby-scale app that does what we did.

And the code?

Then came the implementation. This was also not one-shot, and we don't have a mathematical proof that the Rust code conforms to the model. What we have instead:

• Lockstep conformance tests. The new save engine is written as an explicit state machine whose steps a test scheduler can advance one at a time. Every model scenario is replayed against the real code, in each of the four race profiles, plus random walks. Between any two disk operations the test may inject what the model allows there: an external write, an app crash, a power cut. After every step, the code's state is compared field by field with the model's.
• A simulated filesystem that really loses data. Those tests run on a model filesystem that can drop anything not yet synced to disk at a power cut, including a rename that wasn't made durable. Drafts are real files in it, so recovery runs the actual launch code.
• Forbidden actions. The tests also try things the model says can't happen yet (a second save while one is running, a rename of a page with unsaved edits) and check that the code waits or refuses; the tests ask the real code for its refusal rather than assuming it. In three spelled-out cases the code is stricter than the model and refuses where the model would proceed; each is checked to change nothing, and a planted unnecessary refusal must be caught.
• Mutation testing. The deliberately broken model variants, mapped to the code, plus hand-made and automatic mutations of the save engine, must each be caught by some test. A mutation that survives must be explained.
• Real filesystems. The production code runs against real disks with injected faults (failed fsync, failed rename, I/O errors), and a matrix of ordinary setups checks that everything that saved before still saves: ext4, btrfs, tmpfs, FAT/exFAT and NFS here, NTFS and APFS on CI.
• Adversarial review of each implementation milestone by another model, over many rounds.

So the chain is: English spec → Quint model (checked) → Lean proof (kernel-checked; the whole guarantee for the current model) → code (tested against the model, not proved). From 0.8.0-beta.2 on, the code is tested against the current model version, the one the proof covers (0.8.0-beta.1 was tested against the previous version, which lacks the later name-slot check and one guard fix). The two weakest links are named: the Lean copy matching the Quint model is checked by replaying scenarios rather than proved, and the code matching the model is tested rather than proved. The model also says nothing about how fast things are saved, and the guarantee is claimed for normal local filesystems; Android/iOS document providers and network drives run the same code on a best-effort basis.

This shipped in 0.8.0-beta.1 as the new background save engine. Does it cost performance? Mostly no, and one thing got faster. Compared with the Beta just before the new engine, on two real-sized graphs: the median time from a keystroke to the text being safely on disk dropped from about 1.3 s to about 0.5 s; launch and deleting a page are unchanged; renaming a page with many references is somewhat slower (about 15% on Linux). On Windows, renames that rewrite hundreds of pages are noticeably slower, because each rewritten file is now written straight through to disk. That trade is deliberate.

The spec, the Quint models, the scenarios and the Lean proofs are in the repository under docs/storage-model/, with a README saying exactly what is proved for which model version.

Why I'm excited

Time will tell whether this has really dealt with a big portion of storage bugs. But I am pretty excited about it: not only because it is good news for Tine's storage layer, but also because it shows promise for using similar techniques on other parts of Tine.

We cannot do the same thing everywhere. The UI, for example, is very complicated and it's not obvious how to formalize it this way. But the bar for this kind of rigor has dropped dramatically, with the models doing the heavy lifting. Model-checked hobby software may be becoming a reality.

[hestratos]

I love these kinds of posts.

One question I have: Could the entire Logseq/Tine model be formalised? The aim would be to ensure that any future improvements proposed or implemented go through this validation process, so we can avoid the usual situation where we think adding something is the right thing to do, only to find a year later that the model is “broken”.

[Dieterbe]

OMG! Say "I'm not a software engineer" or "this is vibe coded" one more time! 🤣

Perhaps worth pointing out that the only reason you need all the conflict detection and resolution, is because there are external applications writing to the same graph, without coordinating with Tine.
If we only had to deal with applications that could coordinate with each other (e.g. tine cli and tine UI), then we could use locks and/or a centralized service to guarantee serialization of operations.
In an alternate universe where we can disavow syncthing, dropbox, and the likes, we could simplify the design

How does it handle failure in the middle of a rename that involves updating many other pages that contain references to the renamed page? does the rust backend acknowledge the whole thing at once or are the ack's more granular (per-operation)? do you use a WAL (write-ahead-log) or similar, such that if some of the writes succeeded and some failed, you could resume the pending ones during crash recovery?

you mentioned the "lockstep conformance tests" on the code. Do these generate a large corpus of scenarios similar to how the model is tested? How does that corpus compare to the model tests?

In three spelled-out cases the code is stricter than the model and refuses where the model would proceed

is it useful to have this deliberate divergence? can we update the model instead?

Mutation testing. The deliberately broken model variants, mapped to the code, plus hand-made and automatic mutations of the save engine, must each be caught by some test. A mutation that survives must be explained.

This is the most confusing sentence out of the whole article. What are model variants? Why do we have multiple? I thought there was one model. Why are some variants deliberately broken? What are mutations to the save engine? (is this referring to running the lockstep conformance tests with additional code injected?) What's a mutation that survives? Is it an output or an input?

real disks with injected faults (failed fsync, failed rename, I/O errors), and a matrix of ordinary setups checks that everything that saved before still saves: ext4, btrfs, tmpfs, FAT/exFAT and NFS here, NTFS and APFS on CI.

To be clear, when you mention the existing filesystems, these are only running in "normal/healthy" mode , right? Because to get them to generate faults, you'd need to mimic the underlying block device, AFAIK. When you say "real disks" here, I think you mean an artifical filesystem that you control to make it fail (which one do you use for this, btw?)

The model also says nothing about how fast things are saved, and the guarantee is claimed for normal local filesystems; Android/iOS document providers and network drives run the same code on a best-effort basis.

I don't know about document providers, but presumably network drives would just offer the same posix API as any other unix filesystem, and therefore wouldn't be all that different from a local filesystem, other than that they would respond a bit slower and may be more likely to have their own internal issues and/or fail io syscalls (which you already test)

each rewritten file is now written straight through to disk. That trade is deliberate

what does this mean? straight, as opposed to what, indirectly? do you mean with some kind of sync/fsync option? do you mean that you run many syscalls concurrently and/or in parallel? (i suspect not, you would probably at most use a pool with a bounded size)

[martinkoutecky]

Written by Claude (Opus 5.5), read and approved by Martin.

@Dieterbe, thanks for the careful read. Everything below is about the current model version, s3.5. Writing it up made me check the post against the receipts, and two of its claims about real filesystems were too broad; corrections are under "real disks" below.

"Conflict detection exists only because of external writers." Half right. The guard check (a save only replaces the exact bytes it based its text on), the conflict handling, and the accepted race R1 exist for writers that don't coordinate with Tine: Syncthing, Dropbox, git, Logseq, or stable and Beta Tine side by side (they are two separate apps with separate app data). In a closed world those parts could go. Two other layers would stay:

• Crashes and power cuts. Drafts, the fsync and rename order, launch recovery and the trash for deletes exist because a process can die between any two system calls. No lock helps with that.
• Tine's own clients. For these we already did what you suggest: one process per graph (the "page host", in the app or in a headless tine serve) owns every page and does all file I/O. The CLI and every window are its clients. They find it through an exclusive lock and a per-user socket, and the CLI starts tine serve if the app isn't running. Even then, clients are asynchronous. A window sends text tagged with the version it was typed on, and that version can be stale by the time it arrives. The hole the Lean proof found (unsent typing silently undoing a CLI delete) involved no outside program at all.

A crash in the middle of a rename. One acknowledgement for the whole operation, and no separate WAL: the drafts play that role. Before the host answers, it writes the new state of every page the rename changes (the new page, every rewritten referrer, the old page's deletion) into one draft file, with a checksummed record per page, made durable by temp, fsync, rename and directory fsync. A failed draft write refuses the operation and changes nothing. The pages are then saved by ordinary guarded saves, in a fixed order: new page first, then the referrers, and the old page goes to the trash last. That order is what the orderHolds property checks.

After a crash, recovery rolls forward, never back. Launch restores every page from the drafts before anything else touches them, and their normal saves finish the rename. The draft file records page states, not a command, so nothing is re-executed. Two honest limits:

• The order is only guaranteed while Tine runs. Between a crash and the next launch, the disk can hold any partial combination, and a sync tool running then will copy it. Across a crash, the guarantees are no loss and completion at the next launch.
• The guarantee that a renamed page always has a file at its old or new path (renameResolves) also holds only while Tine runs.

Lockstep tests vs model tests. The code side is much smaller than the model side, and not exhaustive. Against the code, all of these are part of the ordinary Rust test suite, which runs before every integration and in CI before releases:

• the 194 hand-written model scenarios in each of the 4 race profiles (776 runs, state compared field by field after every step);
• 32 committed random traces generated from the model (all 256 locally);
• 61 targeted traces the model checker produced to reach rare branches;
• 48 random walks of 800 steps that also try forbidden actions and inject faults.

The model side has the same 194 scenarios, random simulation (4 × 4,000 runs × 60 steps), bounded TLC runs (the largest complete one: 4.3 billion steps over 2.1 million distinct states), and the Lean proof for every reachable state. Code coverage comes from mapping onto the model's scenarios, not from a corpus of comparable size.

The three stricter cases, and why not update the model. The model decides from the page buffers the host holds. The code also looks at the real disk under its path locks and at its own request queue, so it can see three things the model can't:

1. a twin file (Foo.org next to a new Foo.md) when a save creates a page. The save fails, which the model also allows (saveFail);
2. a file that appeared at a new page's path but hasn't been observed yet. The operation is refused;
3. typed input already queued in the host but not yet applied. An operation on that page is refused.

Each refusal must change nothing (state, readable and durable files, versions, all checked), and each has a planted spurious-refusal mutant that the tests must catch. The opposite direction, code accepting a step the model forbids, is a test failure. Martin chose not to write a model version for these: it would mean more Lean work with no safety gain, since a refusal can't lose data.

Mutation testing, the confusing sentence. Sorry; the sentence packs three things:

• Model mutants (38). Copies of the one model, each with one rule deliberately broken: skip the guard check, delete without trashing, don't draft the rename's new page, and so on. Each must be caught by its own scenario. They test the tests: a property or scenario set that can't catch a planted bug can't be trusted to catch a real one. The shipped model has MUTANT = "none".
• Mapped to the code (66). The same kinds of bug written as edits to the save engine's Rust source. Each is compiled and the page-host tests are run, and every one must fail them.
• Automatic mutations. Tooling that systematically perturbs code (dropping operands of &&/||, cargo-mutants) and reruns the tests. A mutant "survives" if the code is changed and every test still passes. Neither input nor output: it's a finding about the tests. Every survivor must be listed with a written argument for why the change can't be observed; an unlisted survivor fails the report. Those arguments are reasoned by hand, not proved.

The large counts (466 hand-made and 884 cargo-mutants cases) apply to the Rust transcription of the model the tests use as oracle, not to the production engine, which has its own smaller run. The post blurred that.

Real disks. You read it right, and the post overstated it.

• Fault injection is in software, at Tine's own I/O boundary: a test build's file-I/O layer returns an error instead of making the call (failed fsync, failed rename, generic I/O errors), or aborts the process before the nth call. The files are real, and the device isn't involved: no FUSE, dm-flakey or block-device tricks.
• Power cuts happen only in a simulated filesystem. It keeps "readable" and "durable" state apart, and a cut can drop anything not yet synced, including a rename that wasn't made durable.
• Real filesystems ran in healthy mode only. Recorded runs: ext4 and tmpfs here, NTFS in CI. The post's btrfs, FAT/exFAT and NFS were planned but never run (no loop devices or writable NFS on this machine). APFS isn't in CI for the save engine yet, only for backups and file locks. Those are open items now.

Network drives. Mostly POSIX, yes; three differences matter for the claim:

• NFS (and Android's shared-storage FUSE) refuse renameat2(RENAME_NOREPLACE) with EINVAL. Tine then falls back to an absence check plus a plain rename, leaving a microsecond window in which a file created by someone else could be replaced.
• Several NFS and FUSE implementations reject a directory fsync. Tine tolerates that rather than making the graph read-only, so a save it acknowledged there can revert at a power cut. In model terms, that storage is in the weak profile.
• File watching misses changes on some network mounts. Tine polls and rechecks when its window gets focus, so it may notice outside edits later.

Tine doesn't detect a network drive. It reacts to the errors the calls return, and that is why it says "best effort" and not "proved". NFS-specific semantics (close-to-open consistency, attribute caching) aren't modelled.

"Written straight through." On Linux, a save is temp file, fsync, rename, fsync of the directory. Windows has no directory fsync. The new engine therefore publishes each file with MoveFileExW(REPLACE_EXISTING | WRITE_THROUGH), which returns only once the rename's metadata is on disk; the old code used a plain rename. The data was already flushed with FlushFileBuffers before. There's no parallelism and no pool: the host runs one page save at a time, so a rename with 250 referrers pays that cost 250 times in a row. On a GitHub Windows runner that took about 2.5–10 s, against 2.1–2.5 s with a plain rename. Martin chose durability over speed here.

The details are in docs/storage-model/README.md ("The trust gaps" covers the code side).

[martinkoutecky]

OMG! Say "I'm not a software engineer" or "this is vibe coded" one more time! 🤣

Obviously, I'm flattered, but it made me realize something. I really am not a software engineer. I can see that because at our school of computer science there are real software engineers. I am muddling through and having Claude teach me stuff on the way. It is fun and I am learning a lot; I have always learned best when the context was concrete and there was a clear motivation to what I am trying to understand.

We (our university) are obviously thinking a lot about what to tell and teach our students given the state (and trajectory) of AI. This includes software engineering. My very vague take is something like the above -- it's more about meta-skills / postures. Treat the AI as a teacher in domains where you are not an expert. Trust your smell and push where you think AI is being overconfident. Be aware of The Bitter Lesson and recalibrate continuously as new models come out.

If I wasn't a theorist, Tine would not have a proven storage model. But probably it would also not have made the terrible managed storage detour because a true engineer would have recognized the smells way sooner, or steered the agent through those treacherous waters to actually get a working, correct, performant CRDT engine. The respective training still show, but less and less. Who's to say that in a year Claude will simply not decide that it would be a good idea to formalize its storage model and prove its correctness, on its own, without the user asking it to?

So @Dieterbe my question is whether you have any word of wisdom as for what you think is worth teaching as part of an "AI-powered development" course that we are pondering, since you are a true software engineer, unlike me, an imposter ;)

[Dieterbe]

Cool song, and so true. I neither want to derail this thread, nor repeat what i already said in #565 but it seems my point hasn't come through, so I'll be a bit more blunt this time. And repeat myself only this once. You are only seeing university software engineers. You haven't seen the real industry which is full of software engineers with and without diploma's of various degrees, who - I promise you - produce software projects of vastly inferior quality than this one. For many of them, it's mainly the first 5 years after graduation, but many manage to be terrible at their jobs for their whole careers (these types often end up at large enterprises and governments and are responsible for the awful service portals and legacy software that everyone hates). They don't put anywhere near the same level of thought into their process, design, or output. I know many such people. They are still afraid of using AI, they have never even heard the term CRDT. Even among the better engineers, pressures of deadlines, and "agile development" often means rushing to release crap that often works barely good enough. The industry works completely different than the academic world. At my last company, I have personally built software that lost and corrupted data because of stupid bugs or design choices (and lack thereof), and yet.. we had mostly happy customers and supported millions of annual revenue. (that code has been long fixed and/or replaced, of course). The best example is probably mongodb. Check this https://share.google/aimode/tF1owHVUybGVr6JtT - I hope the irony of a tech company - worth billions of dollars - building one of the world's most popular databases, so littered with ridiculous data loss issues, masterfully demonstrated (and ridiculed) by a single hobbyist lacking a software engineering degree, by employing formal systems testing using a very similar approach as what you're doing here, is not lost on you. An approach, which is by the way both extremely uncommon in the industry, and the only way to produce highly reliable systems; as you pointed out. It's so ridiculous and ironic. I couldn't have made this up.
This is not about flattery. You are - by definition - not vibe coding. You employ agentic engineering, which is different.. And you are demonstrably a software engineer, just like the many software engineers without degrees in a highly unregulated industry where anyone can be one.
I agree with what you've said about expectation management for this project; but the answer is better disclaimers about the state of the project, not by misrepresenting the process by which it is built or displaying excessive humility. Consider young people discovering cool projects like this one and the message you want to give them. You are a great example of how anyone can be a software engineer and build good, useful software, regardless of qualification. It's inspiring to others. Don't spread the message that you (and them) can't be good enough.

Who's to say that in a year Claude will simply not decide that it would be a good idea to formalize its storage model and prove its correctness, on its own, without the user asking it to?

Exactly. the role of software engineer is definitely changing, to be more product-driven and work well with the market and with agents rather than with specific lines of code. (but again, there is a lot of heterogeneity in the industry, you have the pioneers leading the charge, the legacy enterprises afraid of touching AI, and everything in between).

I don't want to be a broken record, so I won't repeat these points again. But feel free to ask me specific questions after giving due consideration what I've written here and in #565

As far as the course, the field is changing quite fast. Obviously avoid teaching specific models or techniques which will be legacy quickly. Perhaps there are a few techniques which may last a bit longer (see e.g. https://dieter.plaetinck.be/posts/complementing-an-ai-agent-with-deterministic-tooling-using-swamp/ ). Knowing which tasks are good for llm's and which aren't. e.g. various statistical methods are better off with dedicated tools. Also how to do quality control and feedback loops. Today it's about building agents using LLM's. Next year, probably something else. I think such a course can't be the usual year or multi-year format; you may need to revise the curriculum every 6 months or even faster. And students would need to actually make use of what they learned quickly, by going into the industry quickly.

[Dieterbe]

"Conflict detection exists only because of external writers." Half right. (...) Crashes and power cuts. Drafts, the fsync and rename order, launch recovery and the trash for deletes exist because a process can die between any two system calls. No lock helps with that.

Sure, but those are not conflicts. I was talking about conflicts due to multiple writers. Obviously you need crash recovery

A crash in the middle of a rename. (...) After a crash, recovery rolls forward, never back. Launch restores every page from the drafts before anything else touches them

1. restore is a bit a ambiguous choice of words here right, because it's the "finally putting in place the correct version", not a "restoring an older version" (but it is bringing it in sync with what you saw within the UI, so in that sense i suppose it's a "restore"), does this meake sense?
2. you can't guarantee that nothing else touches a page before you can "restore" it. syncthing, dropbox, logseq, ... can have made changes. In this scenario, would it raise the conflict resolution UI?

The code also looks at the real disk under its path locks and at its own request queue, so it can see three things the model can't (...) Martin chose not to write a model version for these: it would mean more Lean work with no safety gain, since a refusal can't lose data

aha! very interesting. thanks.

Mutation testing, the confusing sentence. (...) test the tests (...)

wow! Very cool. I've never seen mutation testing before.

Fault injection is in software, at Tine's own I/O boundary: a test build's file-I/O layer returns an error instead of making the call (failed fsync, failed rename, generic I/O errors), or aborts the process before the nth call

aha. that makes sense. does this cover a wide range of possible syscall return values (and combinations thereof)?

Power cuts happen only in a simulated filesystem. It keeps "readable" and "durable" state apart

1. is the simulated FS in rust?
2. what's the difference between readable and durable?

Recorded runs: ext4 and tmpfs here, NTFS in CI. The post's btrfs, FAT/exFAT and NFS were planned but never run (no loop devices or writable NFS on this machine). APFS isn't in CI for the save engine yet, only for backups and file locks. Those are open items now.

I think you only need to test one of tmpfs/ext/btrfs; they all offer the same posix API and only differ in implementation details that are outside the scope of tine's testing (correct me if i'm wrong).
FAT is so incredibly old.. but is perhaps still used on USB sticks. It has some limitatons that no other filesystem has (e.g. case insensitivity). We should reconsider if it's worth supporting FAT/exFAT at all. I don't think it is.
NFS also seems quite niche, but if it's not much work to maintain our tests, then we can.

There's no parallelism and no pool: the host runs one page save at a time, so a rename with 250 referrers pays that cost 250 times in a row. On a GitHub Windows runner that took about 2.5–10 s, against 2.1–2.5 s with a plain rename. Martin chose durability over speed here.

I don't have windows expertise to offer suggestions on the exact syscalls, but I will say (regardless of the OS):

1. using some degree of parallelism may be worthwhile
2. latencies are in itself not really the problem. the question is their implication: do they block the UI? Do they prevent the user from doing anything? It seems reasonable to make "logical operations" (so e.g. a rename is the whole operation across all files that need updating) async, and allow the UI to run ahead of what's on disk, without any blocking. the UI could then have an indicator showing if there's any operations in progress. This may already be the case, I'm not sure (?)