cdleary
commented
1 year ago This is a good discussion to have. Some preliminary thoughts off the cuff...
Hypothetically async/await programming model is a little more powerful than what we have with our "static communicating sequential process" networks in XLS. Not in a "turing machine" sense of power (although maybe that too, depending on how you think about the infinite tape part), but a "how expressive it is in practice" kind of way.
Let's put the details of the Rust model aside for a moment and talk about generally what people might be familiar with from co-routines in other languages. In a programming language with generators/coroutines that can be async/await'd, the async function call spawns a new generator/coroutine. In a sense a generator is like a frame that lives on the heap with an indefinite lifetime, and, even aside from handles escaping to different frames and such, they can be spawned under turing complete conditions and arbitrary numbers of times. On the XLS side we base things on (static) CSP actors which have a static configuration for talking to each other. Spinning things up of indefinite numbers with an arbitrary lifetime is not so much a thing in hardware. So you can see how, at some conceptual point, it seems like the expressiveness of full coroutines goes beyond what is found in hardware.
Pulling it back a bit, though, are there probably a subset of computations that could be meaningfully written "as if" they didn't need to worry about bounded/dynamism of resources, we could prove they only do fixed async/awaits, and make the fixed proc network as a convenience for the user. This seems plausible. It's something I would generally bucket as "features for ease of user-entry". Generally in XLS we've tended to focus on latency-insensitive programming, while keeping control over how the computation can map into hardware designs, by structuring it increasingly. Sometimes productivity features, like I'd imagine some async/await veneer to be, can obscure what is going to happen under the hood. But, I could also imagine a lot of things can be written in that style, and you get a nice big productivity boost from doing so, and not have to think about passing messages as much.
As a result, I'm marking this as a long term enhancement for now -- I think it'd be interesting to see what can be done in this direction and how natural the costs / exposure of the lower level semantics could be made to be (as is often the case with features you might think of as "really nice sugar on underlying capabilities") -- it's something you presumably could layer on top of XLS facilities like our static CSP model.
Also kind-of-funny historical note, the static CSP model we use I think was quickly supplanted by the CSP model where actors can spawn other actors (which is embodied in the pi calculus), but that's not the main theory we can use, given we want to directly be able to describe the fixed resources in the hardware system up front.
An admission, though -- having to deal with token values explicitly is annoying, but in some sense it seems like the most powerful way to delimit the partial ordering of communication side effects that the user might be interested in. (There's some convenience/power tradeoff there too I think.) Things like Handel C and some other programming models just nested either "parallel" or "sequential" blocks, which gives you a topological description of parallelism, but I think the graph form expresses more things that we're interested in; e.g. you can identify edges between particular operations and describe properties of that edge, e.g. "make sure those two sends are at least three cycles apart".
proppy
Curious if https://rust-lang.github.io/async-book/01_getting_started/04_async_await_primer.html was considered as a potential syntactic sugar of top
proc,chan,send,recv,tok.It could be an interesting way to bring more concepts from the regular software programming toolbox into hardware design description.