• dsimcha <dsimcha yahoo.com> Mar 22 2011
• Graham St Jack <Graham.StJack internode.on.net> Mar 22 2011
• dsimcha <dsimcha yahoo.com> Mar 22 2011

dsimcha <dsimcha yahoo.com> writes:

Some discussions about std.parallelism have prompted an examination of 
how far D's guarantees against low level data races should extend and 
how safety and practicality should be balanced.  On the one hand, 
coarse-grained multithreading with hard guarantees against low-level 
races is a great thing if it's flexible enough to do what you need it to.

On the other hand, not everything is implementable (at least not 
efficiently or easily) in such a paradigm.  D is a systems language and 
should not force people who want unchecked shared state multithreading 
to either do without it for fight the type system every inch of the way 
(by casting all over the place) to get it.

I've come up with the following proposal, which is implicitly used in 
the design of std.parallelism, but which I think should be made explicit.

1.  All  safe code must be statically checkable and provably free from 
low level data races provided that all  trusted code it calls is 
correctly implemented.  It may not cast away shared, etc.

2.  All  trusted code must guarantee to its clients that calling such 
code from  safe code will not result in low level data races.

3.  All modules that deal with multithreading must document either that:

     a.  They will use the type system to guarantee that low-level data 
races can't happen.

     b.  They will share state freely.

     c.  They will mostly share state freely, but will make guarantees 
about some specific subset.

std.concurrency would be in category a.  core.thread would be in 
category b.  std.parallelism would be in category c.

All code that only uses modules from category a, does not cast away 
shared and does not use __gshared variables can be guaranteed free from 
low level data races even if it is not  safe.

If you want hard guarantees about low level data races, these can be 
achieved with a very small amount of discipline:  Only use modules from 
category a or only use  safe code.  This is easily checkable.  Using 
modules from category b or modules from category c in non- safe code 
should be considered equivalent to casting away shared:  You may do so, 
but you're on your own when it comes to thread safety and you may not do 
it in  safe code.

Graham St Jack <Graham.StJack internode.on.net> writes:

On 23/03/11 11:08, dsimcha wrote:
 Some discussions about std.parallelism have prompted an examination of 
 how far D's guarantees against low level data races should extend and 
 how safety and practicality should be balanced.  On the one hand, 
 coarse-grained multithreading with hard guarantees against low-level 
 races is a great thing if it's flexible enough to do what you need it to.

 On the other hand, not everything is implementable (at least not 
 efficiently or easily) in such a paradigm.  D is a systems language 
 and should not force people who want unchecked shared state 
 multithreading to either do without it for fight the type system every 
 inch of the way (by casting all over the place) to get it.

 I've come up with the following proposal, which is implicitly used in 
 the design of std.parallelism, but which I think should be made explicit.

 1.  All  safe code must be statically checkable and provably free from 
 low level data races provided that all  trusted code it calls is 
 correctly implemented.  It may not cast away shared, etc.

 2.  All  trusted code must guarantee to its clients that calling such 
 code from  safe code will not result in low level data races.

 3.  All modules that deal with multithreading must document either that:

     a.  They will use the type system to guarantee that low-level data 
 races can't happen.

     b.  They will share state freely.

     c.  They will mostly share state freely, but will make guarantees 
 about some specific subset.

 std.concurrency would be in category a.  core.thread would be in 
 category b.  std.parallelism would be in category c.

 All code that only uses modules from category a, does not cast away 
 shared and does not use __gshared variables can be guaranteed free 
 from low level data races even if it is not  safe.

 If you want hard guarantees about low level data races, these can be 
 achieved with a very small amount of discipline:  Only use modules 
 from category a or only use  safe code.  This is easily checkable.  
 Using modules from category b or modules from category c in non- safe 
 code should be considered equivalent to casting away shared:  You may 
 do so, but you're on your own when it comes to thread safety and you 
 may not do it in  safe code.


Sounds good in principal.

I assume that category a code could be  trusted, and that category b and 
c must not be  trusted.

I agree that trying to use the language to discriminate between category 
b and c would be too tricky, especially when you consider the subtleties 
of what is shared and what is not. Documentation is the only viable 
option there.

Are these static checks feasible, and if so, what are the chances of 
getting them into the language anytime soon?

-- 
Graham St Jack

dsimcha <dsimcha yahoo.com> writes:

On 3/23/2011 12:36 AM, Graham St Jack wrote:
 Sounds good in principal.

 I assume that category a code could be  trusted, and that category b and
 c must not be  trusted.


Right, except for the subset of category C code that does make guarantees.

 I agree that trying to use the language to discriminate between category
 b and c would be too tricky, especially when you consider the subtleties
 of what is shared and what is not. Documentation is the only viable
 option there.

 Are these static checks feasible, and if so, what are the chances of
 getting them into the language anytime soon?


The static checks I'm referring to already are in the language, but are 
dependent on the threading library that's being used enforcing them. 
std.concurrency does, making it category a.  core.thread does not, 
making it category b.  std.parallelism does only for a few  trusted and 
 safe functions, making it category c.