On Wednesday, 27 November 2019 at 11:17:12 UTC, Ola Fosheim Grøstad wrote:
> That said, lifetime-names works ok with GC. The lifetime of GC objects lasts until the end of the program, so you can just mark it as "*", i.e. "forever"...

That assumes that you only use GC-scannable pointers of course!

On 11/26/2019 5:07 AM, Timon Gehr wrote:
> You can't say that just because @trusted exists, @safe doesn't need to do any checking either. Calling @live from non-@live or the other way around amounts to an unsafe type cast.

Of course when @live functions are called, they must supply arguments that fit @live rules. When @live functions call other functions, the interface to those functions must agree with @live rules.

This is not in dispute. You don't have to keep hitting me over the head with it :-)


> I want O/B, but only where it makes sense.

I don't disagree with that, either.


>> I suspect it is possible to segregate such operations into separate, non-@live functions,
> 
> It is not possible. What if you store a std.container.Array as a field of a class object and want to borrow the internal data? If you null out the class pointer after borrowing the internal array data, the GC may deallocate the internal array data. @live can't protect against such interactions.

@live never inserts null. It does not change the code at all. It only adds compile time checks. Marking pointers as "Invalid" after they are borrowed is not a code generation or runtime thing, it is purely inside the compiler.

BTW, under O/B rules, if you borrow a pointer to the internal data, the owner of the data structure (i.e. the cless reference) gets marked "Invalid" (not the field in the class) until the pointer is no longer live.


> Inconvenient and unsound. I would have to write @system code, and the compiler wouldn't even alert me that there is a problem if I annotate it @safe.

This is true. The prototype has set up @live to be an attribute independent of @safe/@trusted/@system annotations. The idea is to try it out without disruption of the logic of the latter 3 attributes. If it works well, I anticipate working it in.


>> In your scheme, this issue is resolved by distinguishing the two by annotating the non-GC pointers with `scope`.
>> ...
> Yes, but `scope` does not track the allocator. `scope` restricts lifetime, and possibly aliasing. As I also said, alternatively, and perhaps preferably, we could annotate aliasing restrictions separately, but the accepted DIP1021 already introduces some checking against aliasing outside @live code.

Ok.

>> I understand that the salient difference between your scheme and mine is you attach it to the pointer type while mine attaches it to the function.
> You attach it to the function, but the meaning pertains to pointers. This should be a red flag, but apparently you don't think so.

That's right.


> This makes no sense to me.  It seems rather weird to be debating the merits of proposals without actually taking into account the consequences of each proposal.

The problem is I agree with your technical criticisms of my proposal, you do not have to keep reiterating them.

> I want a method that makes sense, does not break @safe or GC and improves @safe. This can just as well be some new combination.

We're both on the same team here.


>> 1. Doesn't seem to be a way to prevent un-scope pointers from existing and being unsafe.
>> ...
> It doesn't statically prevent memory corruption in @system code. I don't think this is a "problem".

What happens with raw pointers? Would use of them produce a compile time error?


>> 2. The splitting pointers down the middle into two categories: scope and un-scope.
> It appears this split exists after https://github.com/dlang/DIPs/blob/master/DIPs/accepted/DIP1021.md
> 
>> This is a very intrusive and drastic change.
> 
> I think it's less so than splitting functions into two mutually incompatible categories.
> 
>> The only saving grace of the existing `scope` and `return` annotations is the compiler can infer the vast bulk of them.
> 
> But now there's DIP1021, which checks (unsoundly) that `scope` pointers don't alias. This is not my invention and I would be on board with reverting the decision on DIP1021.
> 
>> Will people accept manually adding `scope` to a big chunk of their types? I don't know.
> 
> If those types want manage memory manually and expose the internal memory directly to a @safe caller, yes.
> If the @safe caller wants to pass around manually-managed memory it will have to annotate stuff as `scope`. This is also true with @live.

The difference is that `scope` is inferred for parameters for templates, auto return functions, and lambdas. `scope` for local pointers is inferred for all functions. This works out rather nicely in practice such that most of the time, the user doesn't need to add any annotations. I am not seeing this happening with your proposal.

I also find concerning the idea that one can have a pointer to a scope pointer - how can that work with O/B?


> If you want to avoid intrusive and drastic language changes, what about reverting DIP1021,

It's currently enabled only with a switch. It's well worth seeing how it works in practice before deciding.

> moving aliasing checks to run time?

Selling runtime checks is a tough battle.

> We could add opBorrow and opUnborrow primitives. opBorrow would return a scoped value borrowed from the receiver and opUnborrow would be called once the last borrow ends. This would even be quite a bit more precise than doing everything in the type system, because you would only prevent invalidation, not all mutation.

I've resisted similar things before on performance grounds. Rust has done a pretty good job selling safety as a compile time phenomenon.

On 01.12.19 10:16, Walter Bright wrote:
> On 11/26/2019 5:07 AM, Timon Gehr wrote:
>> You can't say that just because @trusted exists, @safe doesn't need to do any checking either. Calling @live from non-@live or the other way around amounts to an unsafe type cast.
> 
> Of course when @live functions are called, they must supply arguments that fit @live rules. When @live functions call other functions, the interface to those functions must agree with @live rules.
> 
> This is not in dispute. You don't have to keep hitting me over the head with it :-)
> ...

Then this is a bug:
---
@safe:
int* foo(int* p,const int *q)@live;
void main(){
    auto p=new int;
    foo(p,p); // ok
}
---

> 
>> I want O/B, but only where it makes sense.
> 
> I don't disagree with that, either.
> ...

Ok. (I also want it everywhere where it makes sense.)

> 
>>> I suspect it is possible to segregate such operations into separate, non-@live functions,
>>
>> It is not possible. What if you store a std.container.Array as a field of a class object and want to borrow the internal data? If you null out the class pointer after borrowing the internal array data, the GC may deallocate the internal array data. @live can't protect against such interactions.
> 
> @live never inserts null. It does not change the code at all. It only adds compile time checks. Marking pointers as "Invalid" after they are borrowed is not a code generation or runtime thing, it is purely inside the compiler.
> 
> BTW, under O/B rules, if you borrow a pointer to the internal data, the owner of the data structure (i.e. the cless reference) gets marked "Invalid" (not the field in the class) until the pointer is no longer live.
> ...

None of this is pertinent. You suggested it may be possible to segregate operations including GC pointers into non-@live functions, and I explained why it is not possible.

> 
>> Inconvenient and unsound. I would have to write @system code, and the compiler wouldn't even alert me that there is a problem if I annotate it @safe.
> 
> This is true. The prototype has set up @live to be an attribute independent of @safe/@trusted/@system annotations. The idea is to try it out without disruption of the logic of the latter 3 attributes. If it works well, I anticipate working it in.
> ...

As the goal of @live involves memory safety, I think it is important to specify all interactions of @live with @safe. Otherwise you don't make it clear enough that @live splits the language into two incompatible parts.

> 
>>> In your scheme, this issue is resolved by distinguishing the two by annotating the non-GC pointers with `scope`.
>>> ...
>> Yes, but `scope` does not track the allocator. `scope` restricts lifetime, and possibly aliasing. As I also said, alternatively, and perhaps preferably, we could annotate aliasing restrictions separately, but the accepted DIP1021 already introduces some checking against aliasing outside @live code.
> 
> Ok.
> 
>>> I understand that the salient difference between your scheme and mine is you attach it to the pointer type while mine attaches it to the function.
>> You attach it to the function, but the meaning pertains to pointers. This should be a red flag, but apparently you don't think so.
> 
> That's right.
> 
> 
>> This makes no sense to me.  It seems rather weird to be debating the merits of proposals without actually taking into account the consequences of each proposal.
> 
> The problem is I agree with your technical criticisms of my proposal, you do not have to keep reiterating them.
> ...

Ok. (You are not making that clear when you respond to a technical criticism by reiterating some aspect of @live's design that is superficially related to that point or by claiming that the criticism isn't technical in nature.)

>> I want a method that makes sense, does not break @safe or GC and improves @safe. This can just as well be some new combination.
> 
> We're both on the same team here.
> 
> 
>>> 1. Doesn't seem to be a way to prevent un-scope pointers from existing and being unsafe.
>>> ...
>> It doesn't statically prevent memory corruption in @system code. I don't think this is a "problem".
> 
> What happens with raw pointers?

Nothing happens with raw pointers. Raw pointers are allowed to exist in @safe functions already, and they do not cause memory corruption.

> Would use of them produce a compile time error?
> ...

No.

> 
>>> 2. The splitting pointers down the middle into two categories: scope and un-scope.
>> It appears this split exists after https://github.com/dlang/DIPs/blob/master/DIPs/accepted/DIP1021.md
>>
>>> This is a very intrusive and drastic change.
>>
>> I think it's less so than splitting functions into two mutually incompatible categories.
>>
>>> The only saving grace of the existing `scope` and `return` annotations is the compiler can infer the vast bulk of them.
>>
>> But now there's DIP1021, which checks (unsoundly) that `scope` pointers don't alias. This is not my invention and I would be on board with reverting the decision on DIP1021.
>>
>>> Will people accept manually adding `scope` to a big chunk of their types? I don't know.
>>
>> If those types want manage memory manually and expose the internal memory directly to a @safe caller, yes.
>> If the @safe caller wants to pass around manually-managed memory it will have to annotate stuff as `scope`. This is also true with @live.
> 
> The difference is that `scope` is inferred for parameters for templates, auto return functions, and lambdas. `scope` for local pointers is inferred for all functions. This works out rather nicely in practice such that most of the time, the user doesn't need to add any annotations. I am not seeing this happening with your proposal.
> ...

I don't see why not, but I think this is a criticism of DIP1021, which tries to prevent `scope` pointers from aliasing.

As I have mentioned before, personally, I would prefer to instead have two attributes, `scope` and `owned`. `scope` retains its pre-DIP1021 semantics. `owned` means that there is at most one reference to the annotated data.

> I also find concerning the idea that one can have a pointer to a scope pointer - how can that work with O/B?
> ...

With the attribute split, this would be a pointer to an owning pointer.

I.e., we have an `owned(T)** p`.

While there can be many references to the `owned(T)*`, at most one of them can use it to manipulate the `owned(T)` at any given time.

In particular, dereferencing an `owned(T)**` is not allowed, but we can move the pointed-to owning pointer somewhere else.

Let's say we have a function foo(owned(T)*).

Now foo(*p) cannot work, because this makes a copy of the owning pointer.

However, foo(move(*p)) can work. (`move` would null out *p.)

> 
>> If you want to avoid intrusive and drastic language changes, what about reverting DIP1021,
> 
> It's currently enabled only with a switch. It's well worth seeing how it works in practice before deciding.
> ...

Is it? If you keep inferring `scope` while `scope` disallows aliasing, and that works well enough in practice, why would you not "see that happening with my proposal"?

>> moving aliasing checks to run time?
> 
> Selling runtime checks is a tough battle.
> ...

No matter what you do, the user will need to annotate, have @trusted code and/or do some runtime checking. It's just a matter of balancing them.

The `owned` attribute would allow runtime checks to be elided in the common case. If people don't want to annotate with `owned`, libraries would still be able to fall back to runtime checks.

>> We could add opBorrow and opUnborrow primitives. opBorrow would return a scoped value borrowed from the receiver and opUnborrow would be called once the last borrow ends. This would even be quite a bit more precise than doing everything in the type system, because you would only prevent invalidation, not all mutation.
> 
> I've resisted similar things before on performance grounds.

Fair enough. It's not my preferred solution either. (And my proposals generalize it, because you can borrow out a struct that performs the opUnborrow action in its destructor.)

> Rust has done a pretty good job selling safety as a compile time phenomenon.

I have no interest at all in how Rust is marketed. Rust has bounds checks and runtime checks against unsafe borrowing, because its type system is not expressive enough to formalize functional correctness properties.

On Sunday, 1 December 2019 at 14:44:25 UTC, Timon Gehr wrote:
>> Rust has done a pretty good job selling safety as a compile time phenomenon.
>
> I have no interest at all in how Rust is marketed. Rust has bounds checks and runtime checks against unsafe borrowing, because its type system is not expressive enough to formalize functional correctness properties.

Can you elaborate on this a bit more? Which correctness properties of functions cannot be formalized by rust's type system and what particularly is lacking in it's type system to be able to do that?

If you have any links handy that can explain these concepts also that'd be super appreciated.

Also, can D's type system become expressive enough without being too crazy to solve the same?

On 01.12.19 16:35, aliak wrote:
> On Sunday, 1 December 2019 at 14:44:25 UTC, Timon Gehr wrote:
>>> Rust has done a pretty good job selling safety as a compile time phenomenon.
>>
>> I have no interest at all in how Rust is marketed. Rust has bounds checks and runtime checks against unsafe borrowing, because its type system is not expressive enough to formalize functional correctness properties.
> 
> Can you elaborate on this a bit more? Which correctness properties of functions cannot be formalized by rust's type system

Most of them. E.g., Rust's type system cannot prove that an index is within bounds of a std::vec::Vec.

> and what particularly is lacking in it's type system to be able to do that?
> ...

E.g., dependent types.

> If you have any links handy that can explain these concepts also that'd be super appreciated.
> ...

https://softwarefoundations.cis.upenn.edu/

> Also, can D's type system become expressive enough without being too crazy to solve the same?
> 
In principle, yes. But I am not aiming for this at the moment. Also, people have different ideas about what "too crazy" means.

On 01.12.19 17:04, Timon Gehr wrote:
> 
>> If you have any links handy that can explain these concepts also that'd be super appreciated.
>> ...
> 
> https://softwarefoundations.cis.upenn.edu/

Of course there's also approaches based on program logics/contracts, e.g.:
https://ethz.ch/content/dam/ethz/special-interest/infk/chair-program-method/pm/documents/Education/Courses/SS2017/Program%20Verification/08-Boogie.pdf
https://www.pm.inf.ethz.ch/research/viper.html

In such languages, assertion failures are compile-time errors.

On 01.12.19 17:12, Timon Gehr wrote:
> On 01.12.19 17:04, Timon Gehr wrote:
>>
>>> If you have any links handy that can explain these concepts also that'd be super appreciated.
>>> ...
>>
>> https://softwarefoundations.cis.upenn.edu/
> 
> Of course there's also approaches based on program logics/contracts, e.g.:
> https://ethz.ch/content/dam/ethz/special-interest/infk/chair-program-method/pm/documents/Education/Courses/SS2017/Program%20Verification/08-Boogie.pdf 
> 
> https://www.pm.inf.ethz.ch/research/viper.html
> 
> In such languages, assertion failures are compile-time errors.

Relevant: http://pm.inf.ethz.ch/publications/getpdf.php?bibname=Own&id=AstrauskasMuellerPoliSummers19b.pdf

On Sunday, 1 December 2019 at 16:19:53 UTC, Timon Gehr wrote:
> On 01.12.19 17:12, Timon Gehr wrote:
>> On 01.12.19 17:04, Timon Gehr wrote:
>>>
>>>> If you have any links handy that can explain these concepts also that'd be super appreciated.
>>>> ...
>>>
>>> https://softwarefoundations.cis.upenn.edu/
>> 
>> Of course there's also approaches based on program logics/contracts, e.g.:
>> https://ethz.ch/content/dam/ethz/special-interest/infk/chair-program-method/pm/documents/Education/Courses/SS2017/Program%20Verification/08-Boogie.pdf
>> 
>> https://www.pm.inf.ethz.ch/research/viper.html
>> 
>> In such languages, assertion failures are compile-time errors.
>
> Relevant: http://pm.inf.ethz.ch/publications/getpdf.php?bibname=Own&id=AstrauskasMuellerPoliSummers19b.pdf

Thanks Timon! Much appreciated.

And there foes christmas...

Cheers,
- Ali

FWIW, Microsoft is working on a new research language Verona that partition groups of objects into regions that can have their own memory management scheme. Only one thread can access the same region at the same time as I understand it.

https://www.slideshare.net/KTNUK/digital-security-by-design-security-and-legacy-at-microsoft-matthew-parkinson-microsoft

One of the people behind Pony (Sylvan Clebsch) is listed on one of the slides, and yeah, this approach has some commonalities with Pony, I guess.

Anyway, it is for interacting with C++ code.

On 03/12/2019 11:51 AM, Ola Fosheim Grøstad wrote:
> FWIW, Microsoft is working on a new research language Verona that partition groups of objects into regions that can have their own memory management scheme. Only one thread can access the same region at the same time as I understand it.
> 
> https://www.slideshare.net/KTNUK/digital-security-by-design-security-and-legacy-at-microsoft-matthew-parkinson-microsoft 
> 
> 
> One of the people behind Pony (Sylvan Clebsch) is listed on one of the slides, and yeah, this approach has some commonalities with Pony, I guess.
> 
> Anyway, it is for interacting with C++ code.

I only just watched the talk a couple of hours ago.

There is one key feature that both of us share.
Objects life times get owned by a data structure.

In both of my examples in the code proposal I linked above were based upon just this. Some sort of object (either a class or the double linked lists nodes) is owned by some sort of data structure (Scoped vs DoubleLinkedList).

I am not convinced about their memory region scheme, based upon the talk it looks to be prone to data races with locks. Which is worrying.

But so far I'm getting convinced that my idea isn't completely crazy.

I'm going to try and reach out and get a confirmation on how their memory region system works.