DIP1000

Timon Gehr via Digitalmars-d digitalmars-d at puremagic.com
Tue Aug 30 12:42:22 PDT 2016


On 30.08.2016 18:12, Andrei Alexandrescu wrote:
> I'd like to initiate collaboration on an effort to do DIP1000 rigorously.
>
> First we need to reduce D to a bare subset that only has integers,
> structs, pointers, and functions. That's a working subset of actual D
> code. The grammar I have in mind is at http://erdani.com/d/DIP1000.html.
> ...

- Missing a production rule for ArgumentList.

- There is no ParameterList of length three or more.

- 'return' annotations missing.

> There is no type deduction, member functions, classes, arrays,
> constructors, loops, etc. etc. etc. Only the ability to create
> arbitrarily complex graphs containing integers and pointers to other nodes.
>
> On this language we need to define typing rules and evaluation
> semantics. Once we have those, we need to prove what we want: for scope
> variables the accessibility never outlives lifetime. As a consequence
> we're good to deallocate them early etc.
> ...

I'd just actually deallocate the memory slots when their lifetime ends 
and then prove type safety. (This implies in particular that the 
accessed addressed are still allocated for all dereferencing expressions.)

> The model for typing, evaluation, and proofs is at
> https://www.cis.upenn.edu/~bcpierce/papers/fj-toplas.pdf.

Typing and proofs yes, to some extent, evaluation not really. This paper 
does not allow mutation and does not model memory/aliasing. One 
possibility would be small-step semantics with an explicit heap. (The 
heap would be infinite and never reuse memory slots between allocations. 
This way, memory slots can be reliably marked as already deallocated. 
The stack would not need to be modeled separately, just allocate non-ref 
parameters and locals when entering the function and deallocate them 
when the function exits.)

> It would be
> great if those interested in helping could give the paper a close read.
>
> Once we get this done we'll have a fantastic model for any other
> language changes.
>
>
> Andrei



More information about the Digitalmars-d mailing list