Nondeterminism as an effect

[bblum]

@eholk and I theorise that 'safe' Rust, for not having mutable shared state, currently has two methods for causing nondeterminism - select/fail (fail is basically isomorphic to select in terms of semantics, though implemented differently under the hood), and I/O.

It would be really, really slick if we could prove that one-to-one message-passing is deterministic, and then, pending an effect system, could label all relevant library functions with #[effect(nondeterminism)]. Enterprising users could then #[forbid] it, and be off to... well, NOT be off to the races.

[eholk]

Nondeterministic computations obviously introduce nondeterminism too, such as in if rand() % 2 == 0 { ch.send(5) }.

Also, recv_timeout, which is again isomorphic to select.

[bblum]

do we have a random number generator that uses global state? I didn't know we had one, but I'd consider that to be IO ;)

[eholk]

Oh, right. Yeah, just imagine that rand is implemented by opening /dev/random and reading from it.

[dckc]

Ah... interesting... I've sort of started to audit the library for sources of non-determinism (aka ambient authority). Ideally, libraries would have none; only programs would. If I can achieve this with [forbid...], then that's certainly a start. I'll have to look into it some more...

[thestinger]

Hash tables have unique random keys for the hashing algorithm which determines the order of the key-value pairs. That's going to be a big barrier to implementing anything like this.

[dckc]

Ah. Right.

Back when I saw the hashtable DOS issue, I asked whether E is vulnerable and learned that its hash tables carry an array of the keys (in the order that they were added or something) in order to iterate over them deterministically.

I wonder how much of the rust community would consider this cost-effective.

[thestinger]

They can't contain an array of the keys without using unsafe, so it's not just a performance issue.

I don't think it would be acceptable to increase the size of hash tables by ~50% for an array though since there are other map types available without that property (TreeMap, for example).

There will eventually be a linked hash table type that provides iteration in the order the keys were inserted, but regular hash tables will be much more widely used in the rest of the standard library.

[lkuper]

One way to approach this would be to implement a Kahn process network on top of tasks/pipes and thereby get determinism. It would consist of some number of independent tasks, only communicating with each other over pipes. You'd want to launch all the tasks together at the start, and have all the pipes be open the whole time, so that a try_send couldn't fail due to a pipe being closed. try_recv is already blocking, which matches the semantics of KPNs. importantly, each task could only be waiting on one try_recv at a time. You'd have to leave out select, as @bblum pointed out.

[emberian]

Visiting for triage; carry on.

[thestinger]

Triage bump.

[flaper87]

Triage bump

[thestinger]

A proposal for an effects system and the specific effects would need to go through the RFC process. This issue isn't actionable because it would need to go through an RFC even if fully implemented.