DIP 1024--Shared Atomics--Community Review Round 1

[Ola Fosheim Grøstad]

On Tuesday, 15 October 2019 at 04:09:52 UTC, Manu wrote:
> On Mon, Oct 14, 2019 at 2:50 PM Ola Fosheim Grøstad via 
> Digitalmars-d <digitalmars-d at puremagic.com> wrote:
> I'm aware of a lot of work in this area, but I haven't seem how 
> it
> influences a language at the lowest level (beyond ownership 
> based
> solutions, where transfer of unique ownership is used to model
> thread-safe data transitions);

Well, that's because the research topic is «verification». So 
that is where the culture is, but most programmers have no 
interest in verification, because then they would have to think 
about what they are doing twice... They probably should!! But 
that takes time and we have a global programming culture of 
«fudging» things together :-).  Doesn't mean the ideas cannot be 
leveraged for more mundane purposes with more limited scope than 
verification though.

Rust is the outlier, and as such is quite impressive in the sense 
that they have managed to established a culture where programmers 
accept having to do extra (unnecessary) work to make their 
programs run in exchange for higher confidence of correctness. 
But as you can see in any discussion about Rust vs C++, a large 
number of programmers reject that and hold it against Rust. So 
establishing such a culture is not an everyday phenomenon.

You seemed to suggest that I use Rust, but I personally have no 
need for Rust, as I currently don't have issues that Rust can 
solve.  I might pick it up for mundane reasons like tight webasm 
code generation.

What I find interesting about Rust is the culture that builds up 
around the language semantics. Which certainly is a shift from 
programming cultures that preceded it as far as I can tell.


> it's usually in the realm of  what I
> would call 'framework', although there are many examples of 
> such being blessed by the language.

Ok, so basically anything that is unfamiliar in the D context is 
a «framework», including type systems. Fair enough. («framework» 
is usually used for denoting a set of library types and possibly 
runtime with tight coupling that aims to provide a foundation for 
writing applications in a limited category.)


> Then how do you define thread-local by default, and how do you
> mark/identify data that violates that axiom?

The only reason you need to mark TLS is because it is referenced 
using a different instruction sequence.

So to repeat myself:

Other than that, D does not provide anything beyond 
atomics/barriers. Does it? Everything else is purely syntactical. 
Slam a @-tag around your code and you get to reinterpret and 
thwart the type system. That's a syntactical approach in my mind. 
Not a sound type system approach. Therefore it offers nothing 
over a library type.

> static knowledge of a state machine, known threads are 
> collected into
> a registry, and then state transitions can assert validity 
> against the
> other threads in the pool.

You could do it dynamically, but also statically. Simple example, 
if you can establish that all Reader threads are spawned after 
the Writer thread has ended then you can ellide all the locking 
in the Reader threads. (without the programmer knowing about it).


> that ballpark. It's not a functional language, and we don't 
> have *code* or data access introspection like that.

Doesn't have to be FPL, people do interesting things on the IR 
level, but I am not saying D should, the manpower and knowhow 
isn't here.


> That sort of language goes all in on one very restrictive 
> programming model.

It might, but doesn't have to, programmers can restrict 
themselves to satisfy the verifier. It appears to work for Rust.


> If you want to resist `shared`'s existence, then I don't think 
> ideas like this will move us forward.

I am not resisting anything.

I am trying to figure out why you cannot do «shared» equally well 
as a library type and what is missing in the language that 
prevents that from being possible.

Because if that is not possible then I sense that there must be 
some glaring flaws in the D meta-programming capabilities that 
ought to be fixed.

For me this is an exercise in figuring out what works and does 
not work in D's meta programming model.


> I've read about ideas like this before, but like, it's strictly 
> fantasy. I'm interested in what's real, where we are, what we 
> have, and where we need to be in practical terms.

Ok, so I presented two ends of the spectrum that has a long 
history, one from 1939/1960s (PetriNets) and one from 1980 
(concurrent Hoare logic).  In between those ends you have many 
different approaches.

You wanted to discuss what is possible/not possible, and these 
two end points does say something about what people have been 
researching and therefore what might/might not be possible.

There are probably future applications for concurrent Hoare logic 
in software synthesis (let the computer find instruction 
sequences that satisfy a specification.). At least that seems 
plausible, so I wouldn't call it fantasy or useless.


> There is; D specifies thread-local by default, and that 
> absolutely requires a marker (and associated semantics) to 
> attribute the data that violates that principle.

That's just a claim. No, you only need lower level constructs 
like barriers.

You should be able to implement the marker in a library, if not 
then someone ought to take a hard look at the meta-programming 
capabilities.


> What does this mean to you? We can write very rich libraries 
> with `shared` as a safety mechanism. Nothing more is needed 
> from the language, except perhaps some future implicit cast 
> rules.

That is also not true. If you are allowed to turn "shared" into 
proper "local"  then you've got a type system that is so weak 
that there is no need for it to be in the language. It is not 
sound.

To get a proper and sound type system that requires language 
support you need something stronger than «D shared». Pony's take 
on this is to use more types to mark the legal transitions. Too 
late for D, so you might as well just figure out WHY the meta 
programming capabilities prevent you from implementing «shared» 
as a library type.

I have not been able to figure that out, because nobody has 
showed me why it cannot be done as a library type.


GOLDEN RULE OF THUMB FOR PROGRAMMING LANGUAGE DESIGN:

Before you implement at feature:

1. Implement it as a library solution.

2. Use it and describe why it does not feel right/works right.

3. Figure out what weaknesses the language has that prevents it 
from being done properly as a library solution.

4. Figure out how that can be improved then go back to 1.

5. Give up, evaluate the situation and start planning a language 
feature.


>> It is more realistic that D would expand the type system or 
>> meta-programming mechanisms in ways that are useful to library 
>> authors and that they could create concurrent frameworks.
>
> Right. That's exactly what we're doing. I'm glad you agree :)

I agree with myself, but that is NOT exactly what you are 
doing... :) See the «golden rule of thumb» above.

Before adding a feature, provide an in-depth analysis for why a 
library solution is insufficient.

I don't see how any skilled language designer could disagree with 
that statement.