RFC: document a strict Future contract that forbids snoozing - #4019

Locking primitives could drop their reservations if they are not polled after wakeup. They haven't emitted Poll::Ready to return the lock guard, so the lock is preemptable.

In practice this is impossible without some new "WakeToken" API, where the token must be delivered to the Future that woke up. Otherwise, dropping the token indicates that the future wasn't polled. Mirroring wakers, there could be a "RawWakeTokenVtable" with a consumed and canceled callback, etc.

However I think it is far too late to have something like this but I'd love for this to be proven wrong :)

View changes since the review

They haven't emitted Poll::Ready to return the lock guard, so the lock is preemptable.

If I understand you correctly, I think that's true in the concurrent streams example deadlocks, but not in the others. In the others, the snoozed future holds an actual lock guard, not just a spot in the queue. Footnote 11 also has a playground example of a concurrent streams deadlock with an unfair mutex, where there is no queue, to emphasize that lock fairness isn't essential to the problem.

This is not unsatisfying, this is reflecting the way we can formally reason about liveness properties in a formal framework like LTL.

Saying "promptly" seems to imply some sort of quantitative property, like "within 1 second" or so. From what I understood about the bugs this is intended to fix, that is entirely unnecessary. The only guarantee we truly need is that it will eventually be called. ("eventually" is a formal operator in LTL and a standard ingredient in liveness properties.) How fast it is being called is a quality-of-implementation concern. But any system that arranges for the future to eventually be polled again will eventually make progress, and that is the key formal property that one typically reasons about in this context -- and that is supported by tools (e.g. TLA+), theory, and tons of research.

There are definitely bugs that sit between the two.

Something like:

while let Some(item) = stream.next().await {
    process(item).timeout_ms(1000).await;
}

This doesn't deadlock because the loop body will never await longer than a second, but it's clearly an unintended consequence that the stream futures can sit around "un-polled" for that length of time.

It does seem a lot harder to set up a system when you can prove that this kind of bug does not exist though. Maybe you could treat each Future as a black box and then attempt to prove that progress will be made "eventually" without relying on details inside the future (such as it completing in 1000ms in this case).

It does seem a lot harder to set up a system when you can prove that this kind of bug does not exist though.

Yeah this is more like how I'm thinking about it. This particular loop can't deadlock, but that's sensitive to what we put in the body, so I think it's fair to say that .next() as an individual component isn't living up to the intended contract. We can mix and match components like Timeout and Map and Then without ever causing a deadlock, but components like stream::Next and future::Shared are "deadlock prone". If we wanted to split hairs, we could say that they're not fundamentally broken and that they just need to document extensive requirements for their callers to use them correctly. (As Ralf said, none of this is UB after all.) But realistically, no one wants to ship a .next() method with a bunch of global preconditions and scary warnings attached to it and then blame users for inevitably using it wrong.

The examples I have in my head of someone "exploiting" the finite-period-of-time rule would be something like a runtime that deliberately sleeps for a couple seconds before polling tasks, or a future/stream adapter that spawns a thread to poll its children after a sleep. Obviously(?) we don't want runtimes or components to do silly things like that. But 1) it's not clear to me that there's a formal difference between doing unnecessary synchronous sleeps and e.g. a regular task queue that's just overloaded and bogged down. And 2) doing silly extra sleeps doesn't create non-local conflicts where we need a higher authority to tell us who's wrong; it's just a regular bug.

I could definitely see a case where a runtime might decide to do short sleeps between polls in order to save power say.

"eventually" is a formal operator in LTL and a standard ingredient in liveness properties

We could call this part of the contract the "poll eventually rule" instead of the "poll promptly rule"? It might be a tradeoff between clearly invoking the formal theory, vs describing what implementers should actually do 99% of the time.

I don't think that's the right contract. MaybeNever is allowed to never call the future again

As @oconnor663 said, the implementation always polls the inner future to completion, it just makes whether that completion reaches the caller non-deterministic, so it's definitely possible to satisfy the contract. (Polling the future != the future returning Ready)

Okay, I see now. You basically want to say that I cannot rely on any other future to ever be finished when arguing that I will invoke poll again.

I don't like that. Reasoning based on "that other code I wrote terminates hence this loop will terminate" is pretty standard liveness reasoning. I don't see a good reason to forbid it. I think this just makes the contract harder to understand and harder to reason about without sufficient benefit.

It's also oddly special-cased to wrap all futures in MaybeNever. If for some reason I implement timeout_ms with my own future-like type that's based on my own Poll-like type (and a custom executor that supports them) then obviously it wouldn't get wrapped and hence the new clause would change nothing. I don't see a reason why one would do that, but I also don't see a reason why it should make any difference for whether a given future satisfies the liveness requirements.

Okay, I see now. You basically want to say that I cannot rely on any other future to ever be finished when arguing that I will invoke poll again.

Yes. I think this aligns well with the goal of allowing futures to make independent progress / preventing deadlocks or unwanted pauses.

Reasoning based on "that other code I wrote terminates hence this loop will terminate" is pretty standard liveness reasoning.

The opposite is also pretty standard to reason about with concepts like wait-freedom, where we must be able to prove that any thread can make progress without any other thread progressing. I think there are some pretty strong parallels here actually.

I don't see a good reason to forbid it. I think this just makes the contract harder to understand and harder to reason about without sufficient benefit.

You may be right, but I don't think it's clear cut. This contract is still relatively easy to understand and excludes some very common code bug classes with futures that the simpler contract does not.

It's also oddly special-cased to wrap all futures in MaybeNever.

We are talking about the contract of the Future trait, so it makes sense that it would be special-cased to implementations of that trait, no? Obviously if you made your own future-like trait you could make up whatever contract you want for that trait? That's true even for the simpler contract: someone could make a SnoozableFuture trait where it's allowed to never be polled again.

The opposite is also pretty standard to reason about with concepts like wait-freedom, where we must be able to prove that any thread can make progress without any other thread progressing. I think there are some pretty strong parallels here actually.

The sleep happens in our "thread" (future) though, so we're not relying on other threads.

This contract is still relatively easy to understand

I beg to differ. ;)

We are talking about the contract of the Future trait, so it makes sense that it would be special-cased to implementations of that trait, no?

No. This is about "sources of waiting that are allowed to occur until poll gets called". I don't see why "waiting for a Future to become Ready" should be special there. It's not about the Future the contract is attached to after all, it's about all the other futures elsewhere in the program. There are many sources of waiting and there's no reason to special-case futures.

Like, for instance this is still allowed under your contract:

while let Some(item) = stream.next().await {
    std::thread::sleep_ms(100);
}

That seems kind of silly, to allow this but disallow the equivalent that's entirely built on Futures. (That program is obviously a bad idea, but that's not the point. It upholds unbounded liveness, and I explained above why unbounded liveness is a very desirable property even though there are trivial examples like this where it seems to be utterly useless.)

That's also why the rest of this paragraph is missing the point; it's not about the future the contract is attached to. Obviously MyFuture can decide not to have a contract, but that's entirely separate from the question of whether Future is allowed to wait for MyFuture (if we can prove that a particular MyFuture will definitely eventually be ready). You are essentially saying that Future must eventually be polled again and as caller I can rely on everything I know about the program except that calls to Future:poll are altered in a specific way (non-deterministically replacing Ready by Pending). But no other function call is altered even though obviously any other function could be doing literally the same thing! That has no parallel with anything I've ever seen, causes a lot of complications and problems for everyone who wants to reason about this systematically and formally, and doesn't actually solve any problem.

The more I think about this, the stronger I am opposed. We shouldn't unilaterally alter the user's program, not even for the purpose of hypothetical executions that we only use to define a liveness contract. Let the user reason about the code they actually wrote.

The analogy with wait-freedom also does not hold up.

Wait-freedom is the strongest non-blocking progress guarantee for concurrent data structures,
ensuring that every operation completes in a finite number of steps regardless of interference from
other threads.

(source)

This is true for the original example as well. Your description as "we must be able to prove that any thread can make progress without any other thread progressing" is an inaccurate summary. It's about interference from other thread preventing progress on the current thread, e.g. by making CAS loops fail every single time. No amount of interference can prevent the sleep from completing, which means that the loop that sleeps is indeed wait-free.