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.

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.

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

On Tuesday, 30 August 2016 at 16:12:19 UTC, Andrei Alexandrescu wrote:
> I'd like to initiate collaboration on an effort to do DIP1000 rigorously.
>
> [...]

If I may suggest, a repository with some LaTeX code may be a good idea, especially if the idea is to write things like << If gamma derives a with lifetime l, then gamma derives a' with lifetime l' >> (I mean, diagrams like the ones at page 9 of the paper). Then you could use subscripts/superscripts to associate lifetime to expressions in these graphs and upload on your site a nice readable pdf.

By the way, do you want to formalize with the aforementioned notation the D subset? If that's the case, I'd really like to help (even if I don't have much time).

On Tuesday, 30 August 2016 at 16:27:05 UTC, Lodovico Giaretta wrote:
> On Tuesday, 30 August 2016 at 16:12:19 UTC, Andrei Alexandrescu wrote:
>> I'd like to initiate collaboration on an effort to do DIP1000 rigorously.
>>
>> [...]
>
> If I may suggest, a repository with some LaTeX code may be a good idea, especially if the idea is to write things like << If gamma derives a with lifetime l, then gamma derives a' with lifetime l' >> (I mean, diagrams like the ones at page 9 of the paper). Then you could use subscripts/superscripts to associate lifetime to expressions in these graphs and upload on your site a nice readable pdf.

Okay this is a bit unrelated to the original question, but it's 2016 and we can do a lot better. It's quite easy to combine LaTeX and Markdowm to get something easy to use and yielding pretty HTML. Have a look at the sources of my blog post from last week:

https://github.com/libmir/blog/blob/master/_posts/2016-08-19-transformed-density-rejection-sampling.md

(As I am quite familiar with the setup and would be happy to set it up - including auto-deploy)

On 08/30/2016 12:27 PM, Lodovico Giaretta wrote:
> On Tuesday, 30 August 2016 at 16:12:19 UTC, Andrei Alexandrescu wrote:
>> I'd like to initiate collaboration on an effort to do DIP1000 rigorously.
>>
>> [...]
>
> If I may suggest, a repository with some LaTeX code may be a good idea,
> especially if the idea is to write things like << If gamma derives a
> with lifetime l, then gamma derives a' with lifetime l' >> (I mean,
> diagrams like the ones at page 9 of the paper). Then you could use
> subscripts/superscripts to associate lifetime to expressions in these
> graphs and upload on your site a nice readable pdf.

Good idea. In fact I'm using a .dd file right now, which can be purposed to generate latex :o).

> By the way, do you want to formalize with the aforementioned notation
> the D subset? If that's the case, I'd really like to help (even if I
> don't have much time).

Correct. Awesome!


Andrei

On 08/30/2016 12:39 PM, Seb wrote:
> On Tuesday, 30 August 2016 at 16:27:05 UTC, Lodovico Giaretta wrote:
>> On Tuesday, 30 August 2016 at 16:12:19 UTC, Andrei Alexandrescu wrote:
>>> I'd like to initiate collaboration on an effort to do DIP1000
>>> rigorously.
>>>
>>> [...]
>>
>> If I may suggest, a repository with some LaTeX code may be a good
>> idea, especially if the idea is to write things like << If gamma
>> derives a with lifetime l, then gamma derives a' with lifetime l' >>
>> (I mean, diagrams like the ones at page 9 of the paper). Then you
>> could use subscripts/superscripts to associate lifetime to expressions
>> in these graphs and upload on your site a nice readable pdf.
>
> Okay this is a bit unrelated to the original question, but it's 2016 and
> we can do a lot better. It's quite easy to combine LaTeX and Markdowm to
> get something easy to use and yielding pretty HTML. Have a look at the
> sources of my blog post from last week:
>
> https://github.com/libmir/blog/blob/master/_posts/2016-08-19-transformed-density-rejection-sampling.md
>
>
> (As I am quite familiar with the setup and would be happy to set it up -
> including auto-deploy)

Isn't it amazing how fast we got to a debate on choosing tools... :o) -- Andrei

On Tuesday, 30 August 2016 at 17:46:41 UTC, Andrei Alexandrescu wrote:
> On 08/30/2016 12:39 PM, Seb wrote:
>> On Tuesday, 30 August 2016 at 16:27:05 UTC, Lodovico Giaretta wrote:
>>> On Tuesday, 30 August 2016 at 16:12:19 UTC, Andrei Alexandrescu wrote:
>>>> I'd like to initiate collaboration on an effort to do DIP1000
>>>> rigorously.
>>>>
>>>> [...]
>>>
>>> If I may suggest, a repository with some LaTeX code may be a good
>>> idea, especially if the idea is to write things like << If gamma
>>> derives a with lifetime l, then gamma derives a' with lifetime l' >>
>>> (I mean, diagrams like the ones at page 9 of the paper). Then you
>>> could use subscripts/superscripts to associate lifetime to expressions
>>> in these graphs and upload on your site a nice readable pdf.
>>
>> Okay this is a bit unrelated to the original question, but it's 2016 and
>> we can do a lot better. It's quite easy to combine LaTeX and Markdowm to
>> get something easy to use and yielding pretty HTML. Have a look at the
>> sources of my blog post from last week:
>>
>> https://github.com/libmir/blog/blob/master/_posts/2016-08-19-transformed-density-rejection-sampling.md
>>
>>
>> (As I am quite familiar with the setup and would be happy to set it up -
>> including auto-deploy)
>
> Isn't it amazing how fast we got to a debate on choosing tools... :o) -- Andrei

Sorry, please ignore, but it would still be nice to put it on Github, so that we can make pull requests. A couple of nits from a first pass:

- ArgumentList is not defined -> ParameterList
- The parameters is limited to 0,1,2 - on purpose? (opt -> * would allow arbitrary numbers of parameters)
- In contrast to FeatherweightJava the grammar allows a lot of weird stuff like:

ref int** foo {
   42 = 42;
   return null;
   *42 = &42;
}

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

On 30.08.2016 21:27, Seb wrote:
>
> Sorry, please ignore, but it would still be nice to put it on Github, so
> that we can make pull requests. A couple of nits from a first pass:
>
> - ArgumentList is not defined -> ParameterList

No, it should be ArgumentList, which is a comma-separated list of expressions.

> - The parameters is limited to 0,1,2 - on purpose? (opt -> * would allow
> arbitrary numbers of parameters)
> - In contrast to FeatherweightJava the grammar allows a lot of weird
> stuff like:
>
> ref int** foo {

Parentheses are required by the grammar, no?

>    42 = 42;
>    return null;
>    *42 = &42;
> }

Those would be ruled out by type checking.

On 8/30/16 3:42 PM, Timon Gehr wrote:
> 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.

Cool, thx.

> 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.

Yah. There are a few papers on modeling heaps, it's not difficult.

> 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.)

Ah, neat. Didn't think of that.

Thanks. I'm embarking on a trip right now, but will get to this as soon as I can.


Andrei

On Tuesday, 30 August 2016 at 16:12:19 UTC, Andrei Alexandrescu wrote:
> http://erdani.com/d/DIP1000.html

Return values can't have `scope` annotation? If the container has trusted opAssign, use after free in this case is not accounted for?