Very limited shared promotion

[Ola Fosheim Grøstad]

On Saturday, 22 June 2019 at 23:41:49 UTC, Manu wrote:
> And in this case, the compiler may treat the scope ref as if it 
> remained thread local and freely ignore the possibility of 
> synchronisation issues, because that's the reality made 
> possible by @safe. Any @trusted code must maintain those 
> assumptions.

Although, it isn't quite as simple, since there are many factors 
that play into this. Including the specifics of the compiler 
optimization level and the concrete hardware (x86 does a lot to 
maintain cache coherency in hardware).

So without language support you risk the compiler repeating all 
the sync work you do in your @trusted code.  Or you risk it 
breaking if you use a compiler with whole program optimization.  
What works with separate compilation does not necessarily work 
with full flow analysis.

But this really depends on the details of the language semantics 
and how far the compiler can go with optimization.  Any 
competitor to C++ ought to do better than C++ when it comes to 
optimization.  Concurrency is an area where there is ample 
opportunity, as concurrency features in C++ are bolted on as an 
after thought. (Very primitive.)

For instance, is the compiler allowed to elide atomic access if 
it marked as nonshared or immutable?  It should be allowed to do 
it (assume it is known that the memory range is nonvolatile).

So, if @trusted means you can do anything, then optimization 
opportunities evaporates.

In my view the type system should be very strict.  I don't think 
@trusted (or even @system) should be allowed to break the core 
guarantees of type system without clearly marking the section and 
how it breaks it using designated language features. So @trusted 
marks that you access language features that are not allowed in 
@safe that could be used in a way that breaks memory safety. What 
you should ask for then is something similar for thread safety.

What you might want to ask for is a rendezvous like language 
feature that temporarily turns nonshared to shared within its 
scope.  Then you can implement parallel for with rendezvous as a 
primitive that the optimizer has to account for. That would be 
much safer than the programmer bypassing the type system without 
any proof that what they do is correct.


Proving correctness for concurrency is very hard, you usually 
have to account for all possible combinations, so to do it in a 
reasonably convincing manner you'll have to build a model that 
proves all combinations.  It isn't something that can be done on 
the back of an envelope.

There are languages/tools for this (some use term rewriting 
languages to do such proofs), but I think it is safe to assume 
that few D programmers know how to do it or are willing to do it 
even if they know how.


In C++ the type system is somewhat non-strict for historical and 
cultural reasons, but as the result the compiler can make few 
assumptions based on types, like with const. (Although they have 
made union more strict than i C). That means that other languages 
in theory can provide better optimization and code gen than C++.

I think languages that want to compete with C++ should focus real 
hard on the weak spots of the C++ type system and find new 
opportunities in that area.


So what you want is a stronger type system (e.g. language 
features like rendezvous), not to allow the programmer to bypass 
and weaken the type system.

Ola.