14 karma · joined July 23, 2023
Such studies may all be flawed in assuming very low utils in designed negative stimuli.
I had an opportunity to play it for a few hours. It's not perfect - it didn't always keep up with my deductions, and on one instance it leaked unknown info via the UI - but on the whole it succeeded at a convincing mechanic.
Oh wow, I've been thinking along these exact lines for a few years; looks like I should have acted sooner! Not that I have any realistic route to be published, arxiv notwithstanding, so it's exciting to see the concept taken up institutionally, and in prestigious ones at that.
I have elsewhere called the concept "programmable pattern matching": when you declare an ADT constructor/variant, you are essentially simultaneously defining a function and a pattern. We already understand how to make functions with custom logic (duh) so the novel contribution is to give the pattern custom logic. And indeed, one possible implementation, which seems very different from the ideas pursued by the article, is to define a function whose signature matches that of the ADT's destructor a la dependently-typed languages (e.g. Lean), except the input is an integer/bitvector of some size instead of an element of the ADT.
To get a better sense of why this is a very exciting idea, check out the development of niche support in Rust enums over the years (e.g. sizeof::<Option<NonNullU8>>() == sizeof::<u8>(), sizeof::<Option<&T>>() == sizeof::<&T>()). The basic concept is there: we want to simultaneously enjoy ADTs which are the best type-safety/memory-safety invention since the invention of types themselves, while enabling every possible trick to save memory as cache lines (or, indeed, elements in the vector/SIMD register file) become a more and more valuable commodity for performance.
They'll still do it, they're just promising not to do it to any right-thinking people.
The disagreement here is rooted in the empirical worldview. Empirically, "rarely" and "never" cannot be (reliably) distinguished, and so adherents of this worldview fail to distinguish claims which are meant to distinguish them.
I'm talking about wfi, wfe, and friends.
Structuring, really?
This is a bit misleading. It's easier to provide mutual exclusion on bare hardware than in an OS; just do a spinlock, except with modern ISAs the core doesn't even spin.
Presumably core doesn't offer this because it's a massive footgun for devs new to multithreading who would not understand why this is unacceptable to use in an OS-hosted process.