Distributed computation, parallelism and (structured) concurrency

[dumblob]

Newbie here. I couldn't find a better place to ask so here I am.

I couldn't find any information about parallelism and concurrency programming in Whiley. Does Whiley as a language have any such support? Does the verification engine support it too?

I'm interested in leveraging multiple (nowadays tens or hundreds on modern smartphones/tablets/notebooks/PCs or "fabric CPUs" etc.) physical cores. So any pure async or green thread like mechanism (incl. structured concurrency is not what I'm asking about here unless it maps to os threads or directly physical/virtual CPU cores (structured concurrency is a good candidate, but I didn't see any such attempt yet).

[DavePearce]

Hey,

Right, its a good question. At this stage the answer, unfortunately, is that it doesn't. Of course, I do want something here, but I haven't figured out the right strategy. I do have some scribblings where I'm trying to figure out the right abstractions to use:

https://github.com/Whiley/RFCs/issues/25 https://github.com/Whiley/RFCs/issues/31 https://github.com/Whiley/RFCs/issues/45 https://github.com/Whiley/RFCs/issues/46 https://github.com/Whiley/RFCs/issues/88

[dumblob]

Thanks for the links. I saw them and I was unable to construct a bigger picture how Whiley wants to proceed with all those options. If you already decided some more bits in that regard, could you sum it up?

[DavePearce]

Hey,

Hmmm, well I don't have an answer to be honest. What I would like is the minimal primitive(s) that allows a wide range of concurrency solutions to be implemented on top. For example, it could be as simple as a compare and swap primitive which would allow locks to be implemented on top. Alternatively, it could be an atomic primitive where certain sequences are guaranteed to compile down to a compare and swap when possible on the given architecture.

On top of this, there is additionally the challenge of how to verify that code using this primitive(s) is free from deadlocks, etc. So, there are some real challenges here. The beauty of designing your own language is that I can ponder these questions for a while before committing to an approach. Right now, I don't need concurrency support in Whiley for it to be useful. At some point, presumably, pressure will start to build though.

[dumblob]

Hey,

Hmmm, well I don't have an answer to be honest. What I would like is the minimal primitive(s) that allows a wide range of concurrency solutions to be implemented on top. For example, it could be as simple as a compare and swap primitive which would allow locks to be implemented on top. Alternatively, it could be an atomic primitive where certain sequences are guaranteed to compile down to a compare and swap when possible on the given architecture.

I know this was just an example, but I'm not sure whether locks/compare_and_swap would be enough to model e.g. transactional memory with all its subtleties. #31 talks about atomic blocks, but it seems distinct. #45 talks about fork but that is being slowly replaced by "spawn" semantics which would make the fork-specific approach soon obsolete (and I can imagine also incompatible with "spawn").

As a side note, first-class (incl. special syntax) support for TM/STM has a high chance to make it into C this year. So it's not any more just a toy :wink:.

Right now, I don't need concurrency support in Whiley for it to be useful. At some point, presumably, pressure will start to build though.

This is a very important point. Thank you for sharing! Should this change, which feed should I follow to stay up to date?

[DavePearce]

Hey,

Well, no ... I am not considering transactional memory at all. To be honest, I don't think hardware transactional memory is really going to be thing. It's interesting what you say about STM going into C ... I would like to know more about that. Do you have any good pointers?

Yes, atomic blocks are a nice solution ... but the question is how to implement them. For example, what happens if there is a failure of some kind? Do we consider roll back? Or perhaps, we restrict what statement kinds can occur in an atomic block.

Ultimately, I normally based my thoughts around what the machine can physically provide. CAS or DCAS primitives (or similar) are what most machines physically provide. They are the only true atomic operations. Therefore, an ideal solution is something which abstracts them sufficiently to generalise across different machines, but doesn't let people shoot themselves in the foot. It also has to allow me to be able to verify stuff around them. Most people wouldn't use them either. Instead, they would use library calls.

One syntax I just considered was a conditional assignment form:

 x = e when c

Here, the assignment only executes when the condition holds true. Otherwise, its a nop. Hence, you would put it into a loop of some kind to check whether the assignment took place.

[dumblob]

Well, no ... I am not considering transactional memory at all. To be honest, I don't think hardware transactional memory is really going to be thing.

From what I saw somewhere, the future is a hybrid approach - not purely hardware TM, but also not purely STM. And I think some modern CPUs already have such "partial" support allowing for building a hybrid TM. But I'm not an expert and we better ask someone researching the topic to tell us what the current state of the art is (at least hardware-wise).

It's interesting what you say about STM going into C ... I would like to know more about that. Do you have any good pointers?

It seems this is an oversight on my side - there is no "Partially merged into C23." on https://en.cppreference.com/w/c/experimental . But yeah, it's mentioned there.

As a side note - I'm mostly interested in decimal floating point being finally natively in C23 (which will be implemented/revised during 2021, and adopted at the end of 2022 according to the schedule).

Yes, atomic blocks are a nice solution ... but the question is how to implement them. For example, what happens if there is a failure of some kind? Do we consider roll back? Or perhaps, we restrict what statement kinds can occur in an atomic block.

If I'm not mistaken C's TM blocks don't allow any failure and they guarantee success (they roll back and retry indefinitely if I'm not mistaken - but maybe there is some HW support to prevent an endless live lock).

Ultimately, I normally based my thoughts around what the machine can physically provide. CAS or DCAS primitives (or similar) are what most machines physically provide. They are the only true atomic operations. Therefore, an ideal solution is something which abstracts them sufficiently to generalise across different machines, but doesn't let people shoot themselves in the foot. It also has to allow me to be able to verify stuff around them. Most people wouldn't use them either. Instead, they would use library calls.

One syntax I just considered was a conditional assignment form:

 x = e when c

Here, the assignment only executes when the condition holds true. Otherwise, its a nop. Hence, you would put it into a loop of some kind to check whether the assignment took place.

Will think about this approach if I find some time.

[DavePearce]

So that report for STM in C looks interesting, though is dated 2015 and I couldn't find heaps of evidence that it's progressing. But definitely and interesting read and seems connected to what I've thinking. I actually know one of the authors so I might reach out to him and see what he thinks the status is!

[dumblob]

Btw. today I came across consistency as logical monotonicity and thought it might be of interest for you in this context if you didn't see it already.

[DavePearce]

Great, thanks!

I had a brief email chat with my friend on that STM C paper. Probably it isn't going anywhere soon. Also, the choice to have both atomic and synchronized blocks was something of a compromise. Personally, I'm not sure how you would implement the atomic blocks as they describe them. I will try to catch up with him in person sometime.

[DavePearce]

The CALM stuff looks interesting, though is something I would imagine being implemented on top of whatever low-level primitives I come up with for Whiley.