The ABI status of filesystem formats [LWN.net]

The ABI status of filesystem formats

Posted Oct 8, 2020 18:04 UTC (Thu) by NYKevin (subscriber, #129325)
Parent article: The ABI status of filesystem formats

My 2¢ (which should not count for much, seeing as I am neither a Linux developer nor someone who regularly works with filesystem images):

This problem would be a lot easier if ext4 had a formal specification saying "This is what a valid filesystem should look like." I'm not really happy with the idea that "valid" just means "something you got from mke2fs(8)." Obviously, people are going to want to do experimental things that are not within the scope of a general-purpose tool like mke2fs. A formal spec would help to delimit the lines between "weird, but supported" and "don't do that, or else you're on your own."

I get the sense that some developers* don't like formal specs. A formal spec does not need to be huge or complicated like the C or POSIX standards; it could just be a short description of what e2fsprogs currently expects and supports, in plain and simple language. In fact, I imagine they could take https://www.kernel.org/doc/html/latest/filesystems/ext4/i..., sweep it for bugs, ambiguities, or outdated information, and then slap a "this is the formal spec" notice on it. This would not necessarily be easy (ambiguities in particular are hard to find and hard to fix), but it wouldn't require convening a huge standards committee or something ridiculous like that.

* This is not a reference to any individual, and it is especially not a reference to Mr. Ts'o. I do not know what Mr. Ts'o thinks of formal specs.

to post comments

The ABI status of filesystem formats

Posted Oct 8, 2020 20:49 UTC (Thu) by khim (subscriber, #9252) [Link] (1 responses)

Format specification only works for simple data structures. Look on C++: it has formal spec, ISO-approved one… yet discussions about if something is a valid C++ or not is not uncommon.

The ABI status of filesystem formats

Posted Oct 8, 2020 22:10 UTC (Thu) by roc (subscriber, #30627) [Link]

C++ is an extreme example. Filesystem formats are vastly simpler than C++. We know how to write formal specifications for quite complicated things.

The ABI status of filesystem formats

Posted Oct 9, 2020 7:11 UTC (Fri) by bangert (subscriber, #28342) [Link] (3 responses)

A formal spec is not the panacea that one may be inclined to assume.

The way i see it, the only thing a formal spec does is to force upon (someone) to take ALL discussions about the subject of the article up front. That's practically impossible to get right and specifically when done well takes a huge amount of effort. If the developers were forced to do it, it would consume their time for a very long time - if someone else were to do it it would/could have a higher degree of defects.

You are highly likely to just debate the formal specification instead of the implementation.

While these objections apply to many situations the extra effort a formal spec introduces is worth it in (some|other) cases.

And although the conclusion of the article, that this subject will likely be discussed again, may be true, that is not in itself a bad thing (and the article does not say so).

The ABI status of filesystem formats

Posted Oct 9, 2020 10:33 UTC (Fri) by roc (subscriber, #30627) [Link] (1 responses)

One nice thing about really formal specs (as opposed to careful English specs, which aren't really formal) is that for many specification languages you can find (or write) tools that leverage the specs to do useful work. For example, for a language like Alloy, fuzzing and model-checking tools can automatically generate testcases that are valid according to the spec and exercise all or most of the interesting edge cases (including many that the spec authors didn't think of).

You may also be able to prove useful consistency properties from the spec, e.g. that a "valid" filesystem doesn't have unaccounted-for blocks, etc.

The ABI status of filesystem formats

Posted Oct 9, 2020 10:35 UTC (Fri) by roc (subscriber, #30627) [Link]

What I meant to add was: if you write formal specifications the right way, you can use these tools to get more value out of the spec, which tilts the cost/benefit tradeoff towards formal specifications.

The ABI status of filesystem formats

Posted Oct 13, 2020 3:29 UTC (Tue) by marcH (subscriber, #57642) [Link]

> The way i see it, the only thing a formal spec does is to force upon (someone) to take ALL discussions about the subject of the article up front.

No, you can write a spec that formalizes an implementation. This is how most RFCs are written.

The ABI status of filesystem formats

Posted Oct 10, 2020 19:43 UTC (Sat) by error27 (subscriber, #8346) [Link] (2 responses)

The problem is that we don't care about a spec, we care about "User space used to work and now it doesn't." So the fix is to program a lot of validation into the kernel so that Josh's filesystem never works from square one. If it never worked to begin with then it can never be broken. It's a lot of work to code this and it doesn't necessarily make Josh any happier.

So probably that approach is a waste of time.

The ABI status of filesystem formats

Posted Oct 11, 2020 19:55 UTC (Sun) by NYKevin (subscriber, #129325) [Link] (1 responses)

> So probably that approach is a waste of time.

I find this remark deeply confusing, so much so that I think I must have misunderstood you.

I proposed creating a formal spec, and declaring that to be the defining line of "what the kernel is prepared to support." In response to this, you described what happens if you don't have a spec and/or don't care about said spec, and then ambiguously said "that approach is a waste of time."

It sounds as if you were trying to refute my suggestion, but your argument before this line appears to *agree* with me, because it describes problems that arise when you don't have a spec. So, if you could clarify your position, that would help me to understand your argument a lot better.

The ABI status of filesystem formats

Posted Oct 12, 2020 13:46 UTC (Mon) by error27 (subscriber, #8346) [Link]

I didn't mean writing a spec is a waste of time. Specs are good because they encourage rigorous thinking. I meant it would be very difficult and a waste of time to try detect filesystems like Josh's in advance and prevent them from mounting.

But although specs have their uses, in the kernel, specs cannot work in the way you have said. The rule is never "You can't break the spec." The rule is "You can't break userspace."

Here is an example. Ten years ago glibc changed memcpy(). https://lwn.net/Articles/414467/ The spec said that the new implementation of memcpy() was valid but kernel developers find this attitude rage inducing. We would never do that in the kernel. You could theoretically still change memcpy(), but first you would have to fix all the applications that rely on the old behavior.

In the glibc example, it's not the flash developers who suffered, it's the regular Linux users. For the users, they had a program which worked and now it doesn't work. They don't care about specs. As kernel developers we care about users first and the spec second.