test suite for complicated cases [LWN.net]

test suite for complicated cases

Posted Jun 22, 2024 15:17 UTC (Sat) by aszs (subscriber, #50252)
Parent article: Rust for filesystems

I'm a little surprised there's no mention here about building a test suite for these "complicated cases" -- that's the obvious way to make sure two independent implementations conform. And it has some benefits:
* the grunt work doesn't have to be done by time-constrained core developers
* getting a nice test suite out of this effort could be a good sweetener to motivate Rust-resistant maintainers

to post comments

test suite for complicated cases

Posted Jun 22, 2024 18:41 UTC (Sat) by willy (subscriber, #9762) [Link] (3 responses)

How would you write a test suite that verifies that every filesystem conforms to the current VFS locking rules? Particularly when those locking rules are mostly not written down.

To take an example that I do know...

When you call folio_mark_dirty(), you must guarantee that the folio will not be concurrently truncated from the file (for values of truncate that include operations like hole-punch).

Holding the folio lock is one way to do that. But this is a sleeping lock, so you can't always do that. If the folio is currently mapped by a page table, holding that page table lock guarantees truncation will not complete, and some callers rely on this.

If you have buffer heads attached to the folio, and you have a buffer head locked, then that is also sufficient to prevent truncation. Some callers rely on this.

Now, encode all that information into a type system? Not sure it can be done. And you certainly can't write a test suite for it. Or any reasonable assertion.

I'm a huge fan of test suites. But saying "just write a test suite" without understanding the problem space is not helpful.

test suite for complicated cases

Posted Jun 22, 2024 20:06 UTC (Sat) by mathstuf (subscriber, #69389) [Link]

One way would be to have some "token" ZST (zero-size type) that one could retrieve from any of these locking mechanisms. `folio_mark_dirty()` would then require that as one of its parameters. Something like:

```
let folio_lock = folio.lock();
let mark_dirty_allowed = folio_lock.i_want_to_mark_dirty();

// …

let buffer_head_lock = buffer_head.lock();
let mark_dirty_allowed = buffer_head_lock.i_want_to_mark_folio_dirty(&folio)?; // better error handling, but checks that it is attached

// ….

let page_table_lock = page_table.lock();
let mark_dirty_allowed = page_table_lock.i_want_to_mark_folio_dirty(&folio); // similar to above; make sure this page table maps the folio
```

Techniques from ghost_cell[1] can likely be used to ensure that the "mark_dirty_allowed" proof token is associated with the folio in question and not any folio that might also exist.

[1] https://docs.rs/ghost-cell/latest/ghost_cell/

test suite for complicated cases

Posted Jun 23, 2024 3:53 UTC (Sun) by aszs (subscriber, #50252) [Link]

Maybe I missed something but it didn't seem that the problem being discussed here was how to "verify that every filesystem conforms to the current VFS locking rules" but rather how to make sure the semantics of the Rust APIs for writing file systems match the semantics for the C APIs for writing file systems -- even as those semantics are changed developers that might ignore the Rust bindings. And if it's unrealistic to test all the ways a surface API might impact some internal invariant, well that's what fuzz testing is for. To be clear, I wasn't saying "just" write a test suite, I was saying I'm surprised tests aren't being discussed as part of a solution to a fairly hard problem.

test suite for complicated cases

Posted Jul 4, 2024 2:34 UTC (Thu) by mrugiero (guest, #153040) [Link]

> Now, encode all that information into a type system? Not sure it can be done.

There's the option to not do that in Rust, too. The type system is quite useful most of the time, but there is a point of diminishing returns and at that point you rely on runtime checks and discipline just like in any other language.

test suite for complicated cases

Posted Jul 15, 2024 2:49 UTC (Mon) by ssokolow (guest, #94568) [Link] (1 responses)

...but do also keep this quote in mind:

Program testing can be a very effective way to show the presence of bugs, but it is hopelessly inadequate for showing their absence. -- Edsger W. Dijkstra, "The Humble Programmer" (1972)

test suite for complicated cases

Posted Mar 17, 2025 20:01 UTC (Mon) by ma4ris8 (guest, #170509) [Link]

With Rust language, formalized reasoning is used increasingly to ensure robustness.

Kani is one of the tools that could be useful.
https://model-checking.github.io/kani-verifier-blog/

Following list is quite impressive, to be checked for more tools:
https://github.com/newca12/awesome-rust-formalized-reasoning