[Swift-devel] swift write once array/struct

[Tim Armstrong]

Agreed, with some of these scripts there are a few questions:

* In what scenarios are there a consistent set of values that could be
assigned to data structures?
* In what scenarios does the language specification guarantee that the
program makes progress and those values are actually assigned?
* In what scenarios does the implementation actually assign the values?

The last two are kind of blurred in Swift since it's not precisely
specified.

E.g. this script is not sensible because there's no consistent value for
the size of the array.

int A[];
if (size(A) == 0) {
  A[0] = 1;
}

This script could reasonably have size(A) == 1 but I don't think it's
reasonable to guarantee progress.
int A[];
if (size(A) == 1) {
  A[0] = 1;
}

This script could reasonably have size(A) == 1, and it might be reasonable
to guarantee progress, since you could have some system where "intent" to
assign the subscript is registered before the subscript is assigned.  I.e.
it goes from EMPTY -> WILL_BE_FULL -> FULL.

int A[];
A[0] = size(A);

Another example might be

int A[];
if (contains(A, 0)) {
  A[1] = x;
}

This example could make progress if the language was smart enough to infer
that A[0] wasn't assigned in the conditional.

I think to better pin down the specification/implementation we probably
need some kind of effect system that models more precisely which bits of
code have what effect on the data structures  -
http://en.wikipedia.org/wiki/Effect_system

We have a prototypical effect system with the write reference counting but
you can have more granular ones where you track which parts of the array
might be modified, etc.

- Tim

On 21 March 2015 at 14:34, Mihael Hategan <hategan at mcs.anl.gov> wrote:

> One more comment.
>
> This is not a deadlock that comes from a faulty implementation, so
> better software engineering won't fix it.
>
> This is an algorithmic issue in that the language allows more
> flexibility that the algorithms implementing it can analyze to determine
> when something that is theoretically deadlock-free would in practice be
> deadlock-free. So there are corner cases where the implementation fails
> not because of something that was missed, but because I don't quite know
> how to do it better.
>
> Mihael
>
> On Sat, 2015-03-21 at 14:16 -0500, Ketan Maheshwari wrote:
> > Thanks Mihael, that clarifies it.
> >
> > Tim, I was thinking from the point of view of avoiding deadlocks. I
> > understand the semantics would remain same. I was thinking a self
> contained
> > array/struct in terms of state management (may be it is called actor
> based
> > impl, not sure) would be more robust in terms of avoiding deadlocks.
> >
> > --
> > Ketan
> >
> > On Sat, Mar 21, 2015 at 12:28 PM, Hategan-Marandiuc, Philip M. <
> > hategan at mcs.anl.gov> wrote:
> >
> > > On Sat, 2015-03-21 at 10:38 -0500, Ketan Maheshwari wrote:
> > > > Hi Tim,
> > > >
> > > > Thanks for the clarification and code snippet. To clarify, in my
> > > > understanding, the implementation is 'extrinsic'.
> > > >
> > > > To be intrinsic, I imagined the array is implemented as an object
> which
> > > has
> > > > a function that monitors and controls its write-once property and
> gets
> > > > invoked every time anything is written to any element of the array.
> > >
> > > The array is implemented as you describe above. I'm not really sure
> what
> > > extrinsic would be.
> > >
> > > Calls to an object's methods aren't automatically synchronized or
> > > atomic, so I don't think that assumption in your earlier email is
> > > correct.
> > >
> > > Even if they were, having this particular method atomic does not
> > > guarantee that there would be no deadlocks. A user can write a[0] =
> > > f(a[1]); a[1] = f(a[0]);
> > >
> > > Mihael
> > >
> > >
>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.mcs.anl.gov/pipermail/swift-devel/attachments/20150321/c26a7ea1/attachment.html>