Safety of unprotected concurrent operations on constant objects

Safety of unprotected concurrent operations on constant objects

[Natasha Kerensikova]

Hello,

sorry to bother you again, but I got lost again in the RM looking for
what I thought was a simple answer to a simple question:

Is it safe to have many tasks performing operations concurrently on
constant objects?


The RM seems only to say things about operations on shared variables
(e.g. in 9.10), which are understandably unsafe (but the guarantee of
safe access to non-overlapping shared variables is a nice once). But
what about concurrent private (presumably read) operations on constants?

It seems obvious that there should be no harm in concurrent reading of
memory, and therefore on concurrent operations on "simple" values, like
scalars or untagged records.

But are there any guarantee on the safety of hidden mechanisms, like tag
checks or dispatching or the implementation of standard containers?
Or could a conforming implementation use internally a splay tree and
make it so that operations on objects declared constant, and indeed
semantically constant, are task-unsafe?


Thanks again for your help,
Natasha

Re: Safety of unprotected concurrent operations on constant objects

[sbelmont700]

On Friday, May 2, 2014 4:42:56 AM UTC-4, Natasha Kerensikova wrote:
> 
> Is it safe to have many tasks performing operations concurrently on
> 
> constant objects?
> 

In the general case, no.  Suppose your constant object is of a private type T, which contains an access value to something else.  Some operation O might read and write to the other object in a non-task safe manner, and so invoking O from two different tasks might cause any number of fun shenanigans.

-sb

Re: Safety of unprotected concurrent operations on constant objects

[Natasha Kerensikova]

On 2014-05-03, sbelmont700@gmail.com <sbelmont700@gmail.com> wrote:
> On Friday, May 2, 2014 4:42:56 AM UTC-4, Natasha Kerensikova wrote:
>> 
>> Is it safe to have many tasks performing operations concurrently on
>> constant objects?
>> 
>
> In the general case, no.  Suppose your constant object is of a private
> type T, which contains an access value to something else.  Some
> operation O might read and write to the other object in a non-task
> safe manner, and so invoking O from two different tasks might cause
> any number of fun shenanigans.

OK, it makes sense.

But then it would be useless to try to encapsulate such an operation in
a function of a protected object, right? Since protected function
provide concurrent access with the only restriction being private
members of the protected object being constant.

And more importantly, that means there is no way of guessing the safety
of concurrent reads without peeking into the implementation, right?

So if I happened to need concurrent read operations (e.g. because
sequencing them through a protected procedure is too inefficient), I
can't use the standard containers. Is that right?

That's quite a setback, having to reinvent containers for something as
weak as concurrent read capability...



Thanks for your help,
Natasha

Re: Safety of unprotected concurrent operations on constant objects

[Simon Wright]

Natasha Kerensikova <lithiumcat@instinctive.eu> writes:

> So if I happened to need concurrent read operations (e.g. because
> sequencing them through a protected procedure is too inefficient), I
> can't use the standard containers. Is that right?

That would certainly be true for some of the Booch Components' Unbounded
forms, which cache the last-referenced element for a performance
improvement if it's re-referenced (I have no idea what evidence Grady
Booch had that that would actually help anyone!). And the way that
implementations of Ada.Containers protect against tampering might cause
problems; the GCC 4.9.0 Vectors has

   type Vector is new Controlled with record
      Elements : Elements_Access;
      Last     : Extended_Index := No_Index;
      Busy     : Natural := 0;
      Lock     : Natural := 0;
   end record;

and Busy and Lock aren't task-safe.

Of course those considerations have nothing to do with whether your
supposedly constant elements are in fact so.

Re: Safety of unprotected concurrent operations on constant objects

[Jeffrey Carter]

On 05/03/2014 02:40 PM, Simon Wright wrote:
>
> Of course those considerations have nothing to do with whether your
> supposedly constant elements are in fact so.

I have no idea what the OP is asking. Values stored in a container are not 
constant. I can't off the top of my head think of anything you can declare with 
the reserved word constant that you couldn't read concurrently. Perhaps an 
example of the case(s) the OP is worried about would help.

-- 
Jeff Carter
"You cheesy lot of second-hand electric donkey-bottom biters."
Monty Python & the Holy Grail
14

Re: Safety of unprotected concurrent operations on constant objects

[Natasha Kerensikova]

On 2014-05-04, Jeffrey Carter <spam.jrcarter.not@spam.not.acm.org> wrote:
> On 05/03/2014 02:40 PM, Simon Wright wrote:
>>
>> Of course those considerations have nothing to do with whether your
>> supposedly constant elements are in fact so.
>
> I have no idea what the OP is asking. Values stored in a container are not 
> constant. I can't off the top of my head think of anything you can
> declare with the reserved word constant that you couldn't read
> concurrently. Perhaps an example of the case(s) the OP is worried
> about would help.

Well, I was worried about standard containers.

I lived quite happily in a single-task world, completely carefree with
regards to concurrency, until I dipped into web programming through AWS,
which introduced to tasking and concurrency hell.

I have some shared resources indexed by a string, described in a
file, and considered as constant throughout the lifetime of the program
(with the standard scheme "restart for changes to take effect").

When I have whatever indexed by a string, I immediately think Maps, and
usually go for Ordered_Maps because they are easier to understand.

Since the map is semantically constant, I use the magic word constant,
with a function to load from file at elaboration, and everything seems
to work fine.

But then I remembered that a few years ago when I looked at the
implementation of GNAT standard containers, they used dirty tricks to
write into fields of an "in"-mode parameter, thereby make it
not-so-constant. From Simon Wright's post I gather this is still the
same.

This made me wonder how magic the word constant actually is, so I posted
here. I naively expected that since the ARM mandated stuff about shared
variable, there would be something in there about shared constant, even
though I couldn't find it.

I later realized that if the word constant is compromised, then
protected functions aren't really protected either, and then there is no
way for anything concurrent to happen safely. Considering that any naive
container is actually safe for concurrent reads, it was a painful
disillusion.

So I guess to correctly frame it as a question, that would be: how can I
have a map capable of concurrent reads with minimal wheel reinvention?
and it looks like the answer definitely doesn't involve any standard
container (unless there is some corner in the ARM that I missed and that
provides some guarantee).

Now I admit I haven't actually encountered any problem yet, since I'm
the only user of the (very early alpha) web application, with at least
seconds between each request, anything non-task-safe would work. But
going with "it works for now, let's worry about this later" isn't really
in Ada spirit, is it?

Re: Safety of unprotected concurrent operations on constant objects

[Dmitry A. Kazakov]

On Sun, 4 May 2014 07:46:00 +0000 (UTC), Natasha Kerensikova wrote:

> Now I admit I haven't actually encountered any problem yet, since I'm
> the only user of the (very early alpha) web application, with at least
> seconds between each request, anything non-task-safe would work. But
> going with "it works for now, let's worry about this later" isn't really
> in Ada spirit, is it?

If you are doing a Web application, then nanoseconds spent on proper
locking should be your least worry. [Of course, you don't not do container
search on the context of a protected action, i.e. it should be a kind of
mutex.]

Certainly there are serious problems with designing containers such that
they were extensible and supported tasking. I would say it is impossible in
Ada right now.

But for a Web application all this does not really matter. You should
concentrate your efforts on efficient requests routing to worker tasks,
ensuring that workers are well-decoupled and don't block each other
externally (via a database or file access, for example) etc.

Using a mutex somewhere in one of hundreds of worker tasks servicing HTTP
requests simply cannot have any effect on either latencies or throughout.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

Re: Safety of unprotected concurrent operations on constant objects

[sbelmont700]

On Sunday, May 4, 2014 3:46:00 AM UTC-4, Natasha Kerensikova wrote:
> 
> So I guess to correctly frame it as a question, that would be: how can I
> 
> have a map capable of concurrent reads with minimal wheel reinvention?
> 

You really can't.  You can either reinvent the wheel in your own task-safe manner, or assume-the-worst about the standard map and surround it with a mutex.  Though, as was said, the split-seconds you would burn on the mutex would be negligible when compared to the network delay of supplying the results.

-sb

Re: Safety of unprotected concurrent operations on constant objects

[Natasha Kerensikova]

On 2014-05-04, sbelmont700@gmail.com <sbelmont700@gmail.com> wrote:
> On Sunday, May 4, 2014 3:46:00 AM UTC-4, Natasha Kerensikova wrote:
>> 
>> So I guess to correctly frame it as a question, that would be: how can I
>> 
>> have a map capable of concurrent reads with minimal wheel reinvention?
>> 
>
> You really can't.  You can either reinvent the wheel in your own
> task-safe manner,

I find it extremely hard to believe that there is no such wheel existing
out there. Standard containers and Booch components might not fit the
particular requirements, but I would bet there are some existing container
implementations that fit.

> or assume-the-worst about the standard map and surround it with a
> mutex.  Though, as was said, the split-seconds you would burn on the
> mutex would be negligible when compared to the network delay of
> supplying the results.

How would you "surround it with a mutex"? Do you mean a procedure in a
procted object, or some other scheme I'm not familiar with?

However, if I start assuming the worst about standard containers, I
might soon slip down the slope towards assuming the worst about all
others standard features. There is nothing in the ARM that prevents tag
checks or dispatching from being implemented through a splay tree or
some other concurrent-read-unsafe mechanism, is there? Should I mutex
those too then?

Re: Safety of unprotected concurrent operations on constant objects

[sbelmont700]

On Sunday, May 4, 2014 11:57:02 AM UTC-4, Natasha Kerensikova wrote:
> 
> How would you "surround it with a mutex"? Do you mean a procedure in a
> 
> procted object, or some other scheme I'm not familiar with?
> 

begin
   Semaphore.Lock
   Map.Find("Something");
   Semaphore.Unlock;
end

where 'Semaphore' is a protected object that blocks when locking, thus serializing any access to the container.  There are of course many other variations on this theme.

> 
> 
> However, if I start assuming the worst about standard containers, I
> 
> might soon slip down the slope towards assuming the worst about all
> 
> others standard features. 
>

And rightly so.  

The problem is not that sharing constant data between tasks is not safe (it is), the problem is that you are assuming internal operation of subprograms, which is bad ju-ju.  For instance:

pi : constant Float := 3.14;

is fine to access from multiple tasks, whereas calling this:

function Get_Pi return Float;

is never safe, even though you are A) not sharing and data and B) the result in question won't ever change.

It's also worth it to point out this portion of the 2012 rationale:

"When the goals of the revision to Ada 2005 were discussed, one of the expectations was that it would be possible to improve the containers, or maybe introduce variants, that would be task safe. However, further investigation revealed that this would not be practicable because the number of ways in which several tasks could interact with a container such as a list or map was large."

-sb

Re: Safety of unprotected concurrent operations on constant objects

[Dmitry A. Kazakov]

On Sun, 4 May 2014 11:30:02 -0700 (PDT), sbelmont700@gmail.com wrote:

> On Sunday, May 4, 2014 11:57:02 AM UTC-4, Natasha Kerensikova wrote:
>> 
>> How would you "surround it with a mutex"? Do you mean a procedure in a
>> 
>> procted object, or some other scheme I'm not familiar with?
> 
> begin
>    Semaphore.Lock
>    Map.Find("Something");
>    Semaphore.Unlock;
> end

Not so. Mutex should always be handled by a controlled "holder" object:

   declare
      Lock : Holder (Resource'Access); -- Seize the resource
   begin
      Map.Find("Something");
   end;    -- Release the resource

This guaranties that the resource will be released even upon an exception
propagation.

Regarding containers it is recommended to use reentrant mutexes if
operations will be extended or if you fancy re-dispatching. An
implementation of reentrant mutex can be found here:

http://www.dmitry-kazakov.de/ada/components.htm#Mutexes

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

Re: Safety of unprotected concurrent operations on constant objects

[Brad Moore]

On 04/05/2014 9:57 AM, Natasha Kerensikova wrote:
> On 2014-05-04, sbelmont700@gmail.com <sbelmont700@gmail.com> wrote:
>> On Sunday, May 4, 2014 3:46:00 AM UTC-4, Natasha Kerensikova wrote:
>>>
>>> So I guess to correctly frame it as a question, that would be: how can I
>>>
>>> have a map capable of concurrent reads with minimal wheel reinvention?
>>>
>>
>> You really can't.  You can either reinvent the wheel in your own
>> task-safe manner,
>
> I find it extremely hard to believe that there is no such wheel existing
> out there. Standard containers and Booch components might not fit the
> particular requirements, but I would bet there are some existing container
> implementations that fit.

I believe as long as the use of the container involves only read 
operations (functions with in parameters), it should be safe to use 
concurrently. Yes, these read operations typically involve modifying the 
container (to implement tamper checking), but is done in such a
way to allow safe concurrent access (at least in the implementations I 
have tried).

If done carefully, concurrent write operations on a container are also 
possible.
For example, I can provide an example in GNAT of incrementing all 
elements in an integer vector container with parallel execution, without 
any added protection or synchronization. Each worker is only updating 
elements in its assigned range of the vector, via Replace_Element. In 
the GNAT implementation, Replace_Element doesn't
set any tampering flags. It only checks for tampering, which might 
happen if another call such as Iterate was executed concurrently.
Since the only call happening during the parallel execution is 
Replace_Element, it works.

That being said, I didn't have any luck finding wording in the RM that
guarantees safe concurrent use of a constant object of a 
language-defined container object. While it likely is safe to do so, if you
are looking for a guarantee, the RM does not appear to provide one 
currently. It might be that this clarification could be added to the RM 
relatively easily, provided that implementers agree that such a 
clarification wouldn't cause too much of an implementation burden.


>
>> or assume-the-worst about the standard map and surround it with a
>> mutex.  Though, as was said, the split-seconds you would burn on the
>> mutex would be negligible when compared to the network delay of
>> supplying the results.
>
> How would you "surround it with a mutex"? Do you mean a procedure in a
> procted object, or some other scheme I'm not familiar with?
>
> However, if I start assuming the worst about standard containers, I
> might soon slip down the slope towards assuming the worst about all
> others standard features. There is nothing in the ARM that prevents tag
> checks or dispatching from being implemented through a splay tree or
> some other concurrent-read-unsafe mechanism, is there? Should I mutex
> those too then?
>

Re: Safety of unprotected concurrent operations on constant objects

[Brad Moore]

On 05/05/2014 1:04 PM, Brad Moore wrote:
> On 04/05/2014 9:57 AM, Natasha Kerensikova wrote:
>> On 2014-05-04, sbelmont700@gmail.com <sbelmont700@gmail.com> wrote:
>>> On Sunday, May 4, 2014 3:46:00 AM UTC-4, Natasha Kerensikova wrote:
>>>>
>>>> So I guess to correctly frame it as a question, that would be: how
>>>> can I
>>>>
>>>> have a map capable of concurrent reads with minimal wheel reinvention?
>>>>
>>>
>>> You really can't.  You can either reinvent the wheel in your own
>>> task-safe manner,
>>
>> I find it extremely hard to believe that there is no such wheel existing
>> out there. Standard containers and Booch components might not fit the
>> particular requirements, but I would bet there are some existing
>> container
>> implementations that fit.
>
> I believe as long as the use of the container involves only read
> operations (functions with in parameters), it should be safe to use
> concurrently.

I need to correct myself. In GNAT any read or write operations on a 
container that set tamper flags are ironically not task safe, so that 
does restrict quite a bit what one can do concurrently.

Re: Safety of unprotected concurrent operations on constant objects

[Shark8]

On 05-May-14 15:23, Brad Moore wrote:
> In GNAT any read or write operations on a container that set tamper
> flags are ironically not task safe

That seems very... odd.

Re: Safety of unprotected concurrent operations on constant objects

[Simon Wright]

Shark8 <OneWingedShark@gmail.com> writes:

> On 05-May-14 15:23, Brad Moore wrote:
>> In GNAT any read or write operations on a container that set tamper
>> flags are ironically not task safe
>
> That seems very... odd.

Rationale 05 8.1 [1] says (last para)

   "The general rule is given in paragraph 3 of Annex A which says "The
   implementation shall ensure that each language defined subprogram is
   reentrant in the sense that concurrent calls on the same subprogram
   perform as specified, so long as all parameters that could be passed
   by reference denote nonoverlapping objects." So in other words we
   have to protect ourselves by using the normal techniques such as
   protected objects when container operations are invoked concurrently
   on the same object from multiple tasks even if the operations are
   only reading from the container."

AARM12 A.18 (5.m) [2] says

   "If containers with similar functionality (but different performance
   characteristics) are provided (by the implementation or by a
   secondary standard), we suggest that a prefix be used to identify the
   class of the functionality: [...] "Ada.Containers.Protected_Maps"
   (for a map which can be accessed by multiple tasks at one time);
   [...]"

Personally I'd like to see the implication (that a standard-compliant
implementation of Containers need not be task-safe unless the Standard
specifies that it must be) made more visible.

[1] http://www.adaic.org/resources/add_content/standards/05rat/html/Rat-8-1.html
[2] http://www.ada-auth.org/standards/12aarm/html/AA-A-18.html#p5.m

Re: Safety of unprotected concurrent operations on constant objects

[Brad Moore]

On 05/05/2014 2:39 AM, Simon Wright wrote:
> Shark8 <OneWingedShark@gmail.com> writes:
>
>> On 05-May-14 15:23, Brad Moore wrote:
>>> In GNAT any read or write operations on a container that set tamper
>>> flags are ironically not task safe
>>
>> That seems very... odd.
>
> Rationale 05 8.1 [1] says (last para)
>
>     "The general rule is given in paragraph 3 of Annex A which says "The
>     implementation shall ensure that each language defined subprogram is
>     reentrant in the sense that concurrent calls on the same subprogram
>     perform as specified, so long as all parameters that could be passed
>     by reference denote nonoverlapping objects." So in other words we
>     have to protect ourselves by using the normal techniques such as
>     protected objects when container operations are invoked concurrently
>     on the same object from multiple tasks even if the operations are
>     only reading from the container.

Except for containers that are already task safe 
(Ada.Containers.Synchronized_Queue_Interfaces)


These paragraph's are actually being revised and are being passed from 
the ARG to WG9 for approval at the June WG9 meeting. If approved, (and 
most likely will be), then the changes apply to the Ada 2012 standard as 
a binding inteterpretation. The changes are mostly clarification to the 
existing intent. The existing wording suggested it only applies to calls 
to the *same* language defined program, whereas the new wording applies 
to calls to *any* language supplied program. Text_IO was also a special 
case when involving standard output. The file parameter is assumed to 
exist, and implicit, so the rule applies to those calls as well.

The new wording is;

  The implementation shall ensure that each language-defined subprogram 
is reentrant in the sense that concurrent calls on any language-defined 
subprogram perform as specified, so long as all parameters that could be 
passed by reference denote nonoverlapping objects.
For the purpose of determining whether concurrent calls on text 
input-output subprograms are required to perform as specified above, 
when calling a subprogram within Text_IO or its children that implicitly 
operates on one of the default input/output files, the subprogram is 
considered to have a parameter of Current_Input or Current_Output (as 
appropriate).

In addition, the following new AARM notes will be added.

" AARM Ramification: So long as the parameters are disjoint, concurrent 
calls on the same language-defined subprogram, and concurrent calls on 
two different language-defined subprograms are required to work. But 
concurrent calls operating on overlapping objects (be they of the same 
or different language-defined subprograms) are NOT required to work 
(being erroneous use of shared variables) unless both subprograms are 
required to pass the associated parameter by-copy.
This rule applies to all language-defined subprograms, including those 
defined in packages that manage some global state (like environment 
variables or the current directory). Unless specified above, such 
subprograms need to work when the explicit parameters are not 
overlapping; in particular, the existence of the global state is not 
considered. Packages with global state may require some locking in order 
to avoid violating this rule."


>
> AARM12 A.18 (5.m) [2] says
>
>     "If containers with similar functionality (but different performance
>     characteristics) are provided (by the implementation or by a
>     secondary standard), we suggest that a prefix be used to identify the
>     class of the functionality: [...] "Ada.Containers.Protected_Maps"
>     (for a map which can be accessed by multiple tasks at one time);
>     [...]"


Another relevant RM paragraph is;

RM 9.10(11-15) which starts;

"Given an action of assigning to an object, and an action of reading or 
updating a part of the same object (or of a neighboring object if the 
two are not independently addressable), then the execution of the 
actions is erroneous unless the actions are sequential."

>
> Personally I'd like to see the implication (that a standard-compliant
> implementation of Containers need not be task-safe unless the Standard
> specifies that it must be) made more visible.
>
> [1] http://www.adaic.org/resources/add_content/standards/05rat/html/Rat-8-1.html
> [2] http://www.ada-auth.org/standards/12aarm/html/AA-A-18.html#p5.m
>

The synchronized keyword in the visible part of the specification of 
Ada.Containers.Synchronous_Queue_Interfaces provides the cue to the 
programmer that the container is task safe.

I'm thinking I'd actually like to see something like a Task_Safe aspect 
that could be applied to type declarations, and subprograms, that would 
make this more clear to users. Having it in the RM is good, but having 
it in the package spec would be even better.

Eg. For Ada.Containers.Vectors...

type Vector is tagged private
    with
       Constant_Indexing => Constant_Reference,
       Variable_Indexing => Reference,
       Default_Iterator  => Iterate,
       Iterator_Element  => Element_Type,
       Task_Safe         => False;

Then programmers could apply the aspect to their own abstractions, which 
better defines the contract of the subprogram or type.

Re: Safety of unprotected concurrent operations on constant objects

[Dmitry A. Kazakov]

On Mon, 05 May 2014 09:11:05 -0600, Brad Moore wrote:

> Eg. For Ada.Containers.Vectors...
> 
> type Vector is tagged private
>     with
>        Constant_Indexing => Constant_Reference,
>        Variable_Indexing => Reference,
>        Default_Iterator  => Iterate,
>        Iterator_Element  => Element_Type,
>        Task_Safe         => False;
> 
> Then programmers could apply the aspect to their own abstractions, which 
> better defines the contract of the subprogram or type.

Task safety is not a type property. Even for a tagged type an unsafe
operation can be defined later on. For non-tagged types it is even less
clear which operations must be safe and which not.

Furthermore, task-safety cannot be inherited or composed. At least not
without massive overhead to prevent deadlocking when two safe types meet as
mutable parameters of a safe subprogram.

And, just how this contract is supposed to be verified?

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

Re: Safety of unprotected concurrent operations on constant objects

[Brad Moore]

On 05/05/2014 10:36 AM, Dmitry A. Kazakov wrote:
> On Mon, 05 May 2014 09:11:05 -0600, Brad Moore wrote:
>
>> Eg. For Ada.Containers.Vectors...
>>
>> type Vector is tagged private
>>      with
>>         Constant_Indexing => Constant_Reference,
>>         Variable_Indexing => Reference,
>>         Default_Iterator  => Iterate,
>>         Iterator_Element  => Element_Type,
>>         Task_Safe         => False;
>>
>> Then programmers could apply the aspect to their own abstractions, which
>> better defines the contract of the subprogram or type.
>
> Task safety is not a type property. Even for a tagged type an unsafe
> operation can be defined later on. For non-tagged types it is even less
> clear which operations must be safe and which not.
>
> Furthermore, task-safety cannot be inherited or composed. At least not
> without massive overhead to prevent deadlocking when two safe types meet as
> mutable parameters of a safe subprogram.

I agree that such a property is not likely inheritable or composable, 
and I don't think we'd want it to be.  I think conceivably it could 
apply to a type, however. It may be that such an aspect could only be 
applicable to tagged types, and only would apply to the primitive 
subprograms of that type. The aspect, if true would become false for any 
derivations of that type, unless those derived types also explicitly set 
the aspect to True.

  If such an aspect were explicitly specified as false for the standard 
containers, for instance, it would pretty much describe
the state of affairs today that have been mentioned in this thread,
but hopefully more obvious to the user. That is, you really cant count 
on any of the subprograms in the containers as being task safe, even 
though some of them may be in a given implementation.

However, it might make sense to specify certain primitive subprograms of 
a type as being task safe. For instance, the Element subprogram of the 
Ada.Containers.Vectors is task safe in the current GNAT implementation. 
If that subprogram were to have the aspect specified as True in some 
future version of Ada, then users of that container would at least know 
that particular call is guaranteed to be task safe by its contract. This 
should be fairly straight forward for similar calls that do not modify 
the container or the elements of the container.

It gets trickier for subprograms that do modify the object, such as the 
Replace_Element subprogram of Ada.Containers.Vectors. That call is 
currently task safe in GNAT, so long as two tasks do not attempt to 
replace the same element.The usage of the container object in that call 
itself is task safe, as it does not modify state global to the container 
object, but the elements contained in the container are not task safe. 
So if we wanted to specify concurrent usage for such a subprogram, maybe 
you'd need two aspects; Task_Safe, and Task_Safe_Components.

    procedure Replace_Element
      (Container : in out Vector;
       Index     : Index_Type;
       New_Item  : Element_Type)
      with Task_Safe=>True,
           Task_Safe_Components => False;

>
> And, just how this contract is supposed to be verified?
>

I see it more as a contract or promise made by the implementer to the 
users of that subprogram that concurrent calls to the subprogram will 
work. In other words, the implementer has designed the call to be task 
safe, using whatever means, and has committed to keep the call task safe 
in the future, by having that property associated with the subprogram 
specification.

At this point, I have doubts that the compiler could 100% guarantee that 
a subprogram call is task safe, but there are likely rules and
restrictions that could be applied that would allow the compiler to 
catch many problems.

In particular, the aspect could restrict the associated subprogram to
disallow:

(1) Calls on other non-protected subprograms that are not Pure or
     Task_Safe;

(2) Dependence on global variables that are neither atomic nor task nor
     protected.

These would be static checks that could be applied at compile time.

Re: Safety of unprotected concurrent operations on constant objects

[Dmitry A. Kazakov]

On Tue, 06 May 2014 00:00:40 -0600, Brad Moore wrote:

> On 05/05/2014 10:36 AM, Dmitry A. Kazakov wrote:
>> On Mon, 05 May 2014 09:11:05 -0600, Brad Moore wrote:
>>
>>> Eg. For Ada.Containers.Vectors...
>>>
>>> type Vector is tagged private
>>>      with
>>>         Constant_Indexing => Constant_Reference,
>>>         Variable_Indexing => Reference,
>>>         Default_Iterator  => Iterate,
>>>         Iterator_Element  => Element_Type,
>>>         Task_Safe         => False;
>>>
>>> Then programmers could apply the aspect to their own abstractions, which
>>> better defines the contract of the subprogram or type.
>>
>> Task safety is not a type property. Even for a tagged type an unsafe
>> operation can be defined later on. For non-tagged types it is even less
>> clear which operations must be safe and which not.
>>
>> Furthermore, task-safety cannot be inherited or composed. At least not
>> without massive overhead to prevent deadlocking when two safe types meet as
>> mutable parameters of a safe subprogram.
> 
> I agree that such a property is not likely inheritable or composable, 
> and I don't think we'd want it to be.  I think conceivably it could 
> apply to a type, however. It may be that such an aspect could only be 
> applicable to tagged types, and only would apply to the primitive 
> subprograms of that type. The aspect, if true would become false for any 
> derivations of that type, unless those derived types also explicitly set 
> the aspect to True.

If you limit it to primitive operations then much simpler to do this:

   type My_Container is tagged ...; -- All operations are unsafe

   type My_Safe_Container is protected new My_Container with null record;

When inherited from, the compiler would override each primitive operation
and wrap it with a reentrant mutex taken. When an operation gets overridden
its new body is wrapped. Calling operation within a protected action would
be bounded error. At least the compiler would be able to maintain mutexes
of such objects, e.g. order them to prevent deadlocks.

[Better of course, would be to have a decent delegation support]

>> And, just how this contract is supposed to be verified?
> 
> I see it more as a contract or promise made by the implementer to the 
> users of that subprogram that concurrent calls to the subprogram will 
> work.

You can use this contract no more you can verify it. Because the compiler
does not know if a call is concurrent or not.

> At this point, I have doubts that the compiler could 100% guarantee that 
> a subprogram call is task safe, but there are likely rules and
> restrictions that could be applied that would allow the compiler to 
> catch many problems.
> 
> In particular, the aspect could restrict the associated subprogram to
> disallow:
> 
> (1) Calls on other non-protected subprograms that are not Pure or
>      Task_Safe;

But calling a task-safe subprogram from another task-safe subprogram were a
much bigger problem than calling a non-safe subprogram. Protected
operations specifically forbid to do exactly this. You could call another
task-safe operation only on the same object and only if the implementation
deploys reentrant locking.

The rules you propose actually are good only for lock-free concurrency.
Unfortunately only few things can be done lock-free, and most types of
containers certainly not.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

Re: Safety of unprotected concurrent operations on constant objects

[Alejandro R. Mosteo]

On Tuesday, May 6, 2014 10:11:07 AM UTC+2, Dmitry A. Kazakov wrote:
> 
> If you limit it to primitive operations then much simpler to do this:
> 
>    type My_Container is tagged ...; -- All operations are unsafe
> 
>    type My_Safe_Container is protected new My_Container with null record;

Ah, how have I longed for such a feature... 

> 
> -- 
> 
> Regards,
> 
> Dmitry A. Kazakov
> 
> http://www.dmitry-kazakov.de

Re: Safety of unprotected concurrent operations on constant objects

[G.B.]

On 06.05.14 10:48, Alejandro R. Mosteo wrote:
> On Tuesday, May 6, 2014 10:11:07 AM UTC+2, Dmitry A. Kazakov wrote:
>>
>> If you limit it to primitive operations then much simpler to do this:
>>
>>     type My_Container is tagged ...; -- All operations are unsafe
>>
>>     type My_Safe_Container is protected new My_Container with null record;
>
> Ah, how have I longed for such a feature...

The usefulness, I think, of safe containers depends on whether or not
containers provide sufficient abstraction.

Convenience aside:

If the program computes with "just data", using more or less
nothing but "indexing", then containers might provide the
necessary (low) level of abstraction. If it's about STL style
"algorithms".

If the program uses containers only to provide some internal
storage, then it will naturally shield them. Its own
data structures (tagged types, say) will only Have-A container,
and not emphasize the container operations.  In this case, I think,
it is adequate to let the programmer place mutex as needed.
(Even re-entrant (owned) semaphores incur some overhead.)

Re: Safety of unprotected concurrent operations on constant objects

[Dmitry A. Kazakov]

On Tue, 06 May 2014 11:49:01 +0200, G.B. wrote:

> If the program uses containers only to provide some internal
> storage, then it will naturally shield them. Its own
> data structures (tagged types, say) will only Have-A container,
> and not emphasize the container operations.  In this case, I think,
> it is adequate to let the programmer place mutex as needed.
> (Even re-entrant (owned) semaphores incur some overhead.)

The issues with this low-level approach are multiple:

1. It is very simple to forget to place mutex in some operation and get a
very nasty bug to find.

2. A language-supported mechanism does not dictate certain implementation.
The compiler may choose monitor instead of mutex or scheduling technique to
achieve the goal in most effective manner.

3. The low-level approach breaks under inheritance especially when
overriding must call to the parent type operations.

4. The low-level approach breaks encapsulation. If you add new operations
you must expose the mutex to them.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

Re: Safety of unprotected concurrent operations on constant objects

[G.B.]

On 06.05.14 14:19, Dmitry A. Kazakov wrote:
> On Tue, 06 May 2014 11:49:01 +0200, G.B. wrote:
>
>> If the program uses containers only to provide some internal
>> storage, then it will naturally shield them. Its own
>> data structures (tagged types, say) will only Have-A container,
>> and not emphasize the container operations.  In this case, I think,
>> it is adequate to let the programmer place mutex as needed.
>> (Even re-entrant (owned) semaphores incur some overhead.)
>
> The issues with this low-level approach are multiple:

OK, for the sake of a more complete list off issues with
either choice:

> 1. It is very simple to forget to place mutex in some operation and get a
> very nasty bug to find.

OTOH, bugs within the task-safe implementation may, as always,
need fixing by the tool vendor; you'd also ask the programmer
to accept that there is either black (not task safe) or white
(task safe), but if he chooses white, he has to suppress his
potential knowledge of a much better concurrency structure.

> 2. A language-supported mechanism does not dictate certain implementation.
> The compiler may choose monitor instead of mutex or scheduling technique to
> achieve the goal in most effective manner.

How could an implementation of task-safe containers be the
most efficient choice for all goals? (I'll assume that, since
"more effective manner" is rather too vague.)

> 3. The low-level approach breaks under inheritance especially when
> overriding must call to the parent type operations.

Everything can break under inheritance, so that's a rather
weak argument, nothing task specific, I think. Clearly, any safe
use of anything in a parent operation can be overridden whenever
the language allows access.

> 4. The low-level approach breaks encapsulation. If you add new operations
> you must expose the mutex to them.

Do you mean "add new operations to the Has-A type"? Chances are
that concurrency control is already associated with the Has-A type,
so adding a new operation to it is not different from adding
operations at all.

Re: Safety of unprotected concurrent operations on constant objects

[Dmitry A. Kazakov]

On Tue, 06 May 2014 14:58:24 +0200, G.B. wrote:

> On 06.05.14 14:19, Dmitry A. Kazakov wrote:
>> On Tue, 06 May 2014 11:49:01 +0200, G.B. wrote:
>>
>>> If the program uses containers only to provide some internal
>>> storage, then it will naturally shield them. Its own
>>> data structures (tagged types, say) will only Have-A container,
>>> and not emphasize the container operations.  In this case, I think,
>>> it is adequate to let the programmer place mutex as needed.
>>> (Even re-entrant (owned) semaphores incur some overhead.)
>>
>> The issues with this low-level approach are multiple:
> 
> OK, for the sake of a more complete list off issues with
> either choice:
> 
>> 1. It is very simple to forget to place mutex in some operation and get a
>> very nasty bug to find.
> 
> OTOH, bugs within the task-safe implementation may, as always,
> need fixing by the tool vendor;

And bugs outside it need not?

> you'd also ask the programmer
> to accept that there is either black (not task safe) or white
> (task safe), but if he chooses white, he has to suppress his
> potential knowledge of a much better concurrency structure.

I don't even understand what this is supposed to mean.

I pointed out that manual wrapping of operations is tedious, error prone,
and the potential damage is incredibly high as bugs may stay undetected in
the production code for years and there is no way to write a test for such
bugs.

>> 2. A language-supported mechanism does not dictate certain implementation.
>> The compiler may choose monitor instead of mutex or scheduling technique to
>> achieve the goal in most effective manner.
> 
> How could an implementation of task-safe containers be the
> most efficient choice for all goals?

By deploying the most efficient method of interlocking available on the
given platform for the given Ada profile.

>> 3. The low-level approach breaks under inheritance especially when
>> overriding must call to the parent type operations.
> 
> Everything can break under inheritance,

This is plain wrong. If everything would break, any program using
inheritance would be broken. Yet there exist non-broken Ada programs that
use inheritance.

I explained how task-safe primitive operations can be overridden remaining
safe.

>> 4. The low-level approach breaks encapsulation. If you add new operations
>> you must expose the mutex to them.
> 
> Do you mean "add new operations to the Has-A type"?

I mean adding an operation, period. This operation, in order to be
task-safe, must use the locking mechanism of the parent type. E.g. mutex.
It means that you must expose the mutex to make the type publicly
extendable.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

Re: Safety of unprotected concurrent operations on constant objects

[G.B.]

On 06.05.14 17:00, Dmitry A. Kazakov wrote:

>>> 1. It is very simple to forget to place mutex in some operation and get a
>>> very nasty bug to find.
>>
>> OTOH, bugs within the task-safe implementation may, as always,
>> need fixing by the tool vendor;
>
> And bugs outside it need not?

They sure need that, too, nothing specific here.

>> you'd also ask the programmer
>> to accept that there is either black (not task safe) or white
>> (task safe), but if he chooses white, he has to suppress his
>> potential knowledge of a much better concurrency structure.
>
> I don't even understand what this is supposed to mean.

It means that in your model, as I understand it, a programmer
gets one of

- *no* operations of a container with sharing related add-ons
   (Ada, as-is)

- *all* operations of a container with sharing related add-ons
   (Ada, with "protected new")

See below for when "protected new" is too much wrap.

> I pointed out that manual wrapping of operations is tedious, error prone,
> and the potential damage is incredibly high as bugs may stay undetected in
> the production code for years and there is no way to write a test for such
> bugs.

Yes. Manual placement of locks etc. is tedious and prone to
error. Locking everything is an alternative, but is going
to annoy those who can show that they do not need everything
locked, or simply cannot afford the additional overhead.

>> How could an implementation of task-safe containers be the
>> most efficient choice for all goals?
>
> By deploying the most efficient method of interlocking available on the
> given platform for the given Ada profile.

So you ask programmers who *do* *know* that concurrent reads are
safe (because they can *show* that concurrent reads are safe)
to still use mutex and not just read concurrently even though
the locks are quite unnecessary?

>>> 3. The low-level approach breaks under inheritance especially when
>>> overriding must call to the parent type operations.
>>
>> Everything can break under inheritance,
>
> This is plain wrong. If everything would break,

("would" invokes the subjunctive conditional, and besides
incurring difficulties, is not "can".)

"everything will break" /= "everything can break"
Conversely,
"some things won't break" /= "some things can't break"

"Protected new" relates to "some things can't break".
"Tagged new" relates to "some things won't break".

You had redefined the meaning of "overriding" by stipulating
that it means "mutex-wrapping-inheritance". That's OK, though,
in real Ada, sadly we don't have that, and whatever a programmer
can access in overriding operations, he can use to break things.
("Can", not "would".) If, by analogy, we could have
"contract-wrapping-inheritance", then nothing could break
either, as long as the contract is good enough and the compiler
can supply the necessary contract-based wrapping.

> I explained how task-safe primitive operations can be overridden remaining
> safe.

Here we are: *every* operation of a so protected container
is run in mutex ways. The programmer does not have a choice.
It may be the best one, or it may be prohibitively slow.

See above.

>>> 4. The low-level approach breaks encapsulation. If you add new operations
>>> you must expose the mutex to them.
>>
>> Do you mean "add new operations to the Has-A type"?
>
> I mean adding an operation, period. This operation, in order to be
> task-safe, must use the locking mechanism of the parent type.

It could use the parent's locking, but it need not, and this
can even be trivially true. (In fact, Ravenscar programs may
require that each client call make use of its own lock, as
there are no queues.)

> E.g. mutex.
> It means that you must expose the mutex to make the type publicly
> extendable.

No, I don't think I need to expose anything. If the type is derived
from a parent whose private parts I cannot see, then my derived
type's operations can only call the allegedly task safe operations of
the parent type. (Which, by assumption, is my Has-A type, which
has a container component, and which itself calls container
operations.)

Re: Safety of unprotected concurrent operations on constant objects

[Dmitry A. Kazakov]

On Tue, 06 May 2014 18:24:24 +0200, G.B. wrote:

> On 06.05.14 17:00, Dmitry A. Kazakov wrote:
> 
>> I pointed out that manual wrapping of operations is tedious, error prone,
>> and the potential damage is incredibly high as bugs may stay undetected in
>> the production code for years and there is no way to write a test for such
>> bugs.
> 
> Yes. Manual placement of locks etc. is tedious and prone to
> error. Locking everything is an alternative, but is going
> to annoy those who can show that they do not need everything
> locked, or simply cannot afford the additional overhead.

If you cannot afford car, there should be none allowed?
 
>>> How could an implementation of task-safe containers be the
>>> most efficient choice for all goals?
>>
>> By deploying the most efficient method of interlocking available on the
>> given platform for the given Ada profile.
> 
> So you ask programmers who *do* *know* that concurrent reads are
> safe (because they can *show* that concurrent reads are safe)
> to still use mutex and not just read concurrently even though
> the locks are quite unnecessary?

No, it is you who is asking programmers to re-invent wheel.

>> I explained how task-safe primitive operations can be overridden remaining
>> safe.
> 
> Here we are: *every* operation of a so protected container
> is run in mutex ways. The programmer does not have a choice.
> It may be the best one, or it may be prohibitively slow.

He clearly has.

> No, I don't think I need to expose anything. If the type is derived
> from a parent whose private parts I cannot see, then my derived
> type's operations can only call the allegedly task safe operations of
> the parent type.

That does not work. Task-safety is non-composable.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

Re: Safety of unprotected concurrent operations on constant objects

[Georg Bauhaus]

On 06/05/14 21:14, Dmitry A. Kazakov wrote:
>> Manual placement of locks etc. is tedious and prone to
>> error. Locking everything is an alternative, but is going
>> to annoy those who can show that they do not need everything
>> locked, or simply cannot afford the additional overhead.
>
> If you cannot afford car, there should be none allowed?

("No car"  is universally quantified, you did that, I opposed it,
asking that there should exist something (in addition?) which is
not universally (mut)exclusive, since some programmers
may have reasons, and proof of safety, to want otherwise.)


>> So you ask programmers who *do* *know* that concurrent reads are
>> safe (because they can *show* that concurrent reads are safe)
>> to still use mutex and not just read concurrently even though
>> the locks are quite unnecessary?
>
> No, it is you who is asking programmers to re-invent wheel.

Programmers may have to use pre-existing wheels (POs, tasks,
simpler ...) to compose a solution. In particular, if they do
not have magic locking that turns every object into a surprisingly
efficient PO.

>>> I explained how task-safe primitive operations can be overridden remaining
>>> safe.
>>
>> Here we are: *every* operation of a so protected container
>> is run in mutex ways. The programmer does not have a choice.
>> It may be the best one, or it may be prohibitively slow.
>
> He clearly has.

If the programmer can request a "protected new" object,
and nothing else beside a "protected new" object, in order
to make a task-safe program, what are the choices, then?
  
>> No, I don't think I need to expose anything. If the type is derived
>> from a parent whose private parts I cannot see, then my derived
>> type's operations can only call the allegedly task safe operations of
>> the parent type.
>
> That does not work.

Yes, it does, as does Ravenscar (not easy), it just does not follow
from only "protected new". Some effort is needed. For example, if
my program's type, the one with the container component part,
is like "protected new", and the consensus protocol is shown to
exclude all tasking issues, my program is task safe.


> Task-safety is non-composable.

Again a universally quantified statement? If you assume that
universal composability is a required feature of every item of
every existing program as well as of every potential program,
then there is little to left to argue.

Re: Safety of unprotected concurrent operations on constant objects

[Dmitry A. Kazakov]

On Wed, 07 May 2014 08:49:08 +0200, Georg Bauhaus wrote:

> I opposed it,
> asking that there should exist something (in addition?) which is
> not universally (mut)exclusive, since some programmers
> may have reasons, and proof of safety, to want otherwise.)

It already exists:

   type Foo is record
       ...
   end record;

>>> So you ask programmers who *do* *know* that concurrent reads are
>>> safe (because they can *show* that concurrent reads are safe)
>>> to still use mutex and not just read concurrently even though
>>> the locks are quite unnecessary?
>>
>> No, it is you who is asking programmers to re-invent wheel.
> 
> Programmers may have to use pre-existing wheels (POs, tasks,
> simpler ...) to compose a solution.

They can even use C. What is the point?

>>>> I explained how task-safe primitive operations can be overridden remaining
>>>> safe.
>>>
>>> Here we are: *every* operation of a so protected container
>>> is run in mutex ways. The programmer does not have a choice.
>>> It may be the best one, or it may be prohibitively slow.
>>
>> He clearly has.
> 
> If the programmer can request a "protected new" object,

The choice is between requesting and not requesting this.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

Re: Safety of unprotected concurrent operations on constant objects

[G.B.]

On 07.05.14 09:40, Dmitry A. Kazakov wrote:

> They can even use C. What is the point?

The point is that

IF programmers want task-safety, and
IF programmers need to respect timing,
-----------
THEN programmers may need to build safe solutions
without "protected new".

The point is that, with "protected new", they cannot get
their job done, in this case.

>> If the programmer can request a "protected new" object,
>
> The choice is between requesting and not requesting this.

The choice is between safety or not, assessing whether or
not things will break, as you claimed they would. Some kinds
of safety nets ("protected new") are so simple and heavy that
this quality may render them inapplicable to some valid
programming problems.

Of which the original problem (reading from a container) is
an example, one that is not resolved by "protected new", it
seems. The "sequential checks" that handle tampering already
add to Ada containers being slow in comparison.

Re: Safety of unprotected concurrent operations on constant objects

[Dmitry A. Kazakov]

On Wed, 07 May 2014 13:25:21 +0200, G.B. wrote:

> On 07.05.14 09:40, Dmitry A. Kazakov wrote:
> 
>> They can even use C. What is the point?
> 
> The point is that
> 
> IF programmers want task-safety, and
> IF programmers need to respect timing,
> -----------
> THEN programmers may need to build safe solutions
> without "protected new".

I don't see where that follows from. Programmers may need do it without
dynamic memory allocation, unconstrained types, tasking, exceptions
whatever. Remove them from the language and anything else they may need go
without. Then we'll talk.

> The point is that, with "protected new", they cannot get
> their job done, in this case.

Which case exactly?

>>> If the programmer can request a "protected new" object,
>>
>> The choice is between requesting and not requesting this.
> 
> The choice is between safety or not,

As well as between drinking beer or not drinking beer, whereas some might
incline to non-alcoholic beer.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

Re: Safety of unprotected concurrent operations on constant objects

[G.B.]

On 07.05.14 14:14, Dmitry A. Kazakov wrote:
> On Wed, 07 May 2014 13:25:21 +0200, G.B. wrote:
>
>> On 07.05.14 09:40, Dmitry A. Kazakov wrote:
>>
>>> They can even use C. What is the point?
>>
>> The point is that
>>
>> IF programmers want task-safety, and
>> IF programmers need to respect timing,
>> -----------
>> THEN programmers may need to build safe solutions
>> without "protected new".
>
> I don't see where that follows from.

"Specification:

1. The concurrent program shall access X safely.
2. It shall do so within at most N µs."

> Programmers may need do it without
> dynamic memory allocation, unconstrained types, tasking, exceptions
> whatever. Remove them from the language and anything else they may need go
> without. Then we'll talk.

Programmers do work in such restricted environments,
for the most part, when using SPARK. Ravenscar was
made to be more efficient than full Ada tasking.
Ada people talk about this.

>> The point is that, with "protected new", they cannot get
>> their job done, in this case.
>
> Which case exactly?

The case which is again listed under "Specification" above.


> As well as between drinking beer or not drinking beer,

Whether or not concurrent reads of Ada containers are both
safe and fast seems unrelated to drinking. Well, unless a drunken
programmer is the cause and the solution of every problem.

Re: Safety of unprotected concurrent operations on constant objects

[Dmitry A. Kazakov]

On Wed, 07 May 2014 15:45:47 +0200, G.B. wrote:

> On 07.05.14 14:14, Dmitry A. Kazakov wrote:
>> On Wed, 07 May 2014 13:25:21 +0200, G.B. wrote:
>>
>>> On 07.05.14 09:40, Dmitry A. Kazakov wrote:
>>>
>>>> They can even use C. What is the point?
>>>
>>> The point is that
>>>
>>> IF programmers want task-safety, and
>>> IF programmers need to respect timing,
>>> -----------
>>> THEN programmers may need to build safe solutions
>>> without "protected new".
>>
>> I don't see where that follows from.
> 
> "Specification:
> 
> 1. The concurrent program shall access X safely.
> 2. It shall do so within at most N µs."

This is not a specification and even less a real-world specification (for
numerous reasons, I don't want to go into). It is an attempt to bring
premature optimization in, by using an imaginary example.

Anyway, mutex access has a factor 2 overhead in terms of protected actions.
BUT, handling container on the context of a protected action would be a
design error in most cases. THEN taking and releasing mutex in Ada is well
below 1µs. A read-write mutex has normally greater overhead than plain
mutex even in read mode. That means, read-write mutex is deployed only when
read operations are lengthy, which is in direct contradiction to your
"specification". Lock-free algorithms do not work with most containers.
Monitors are in order of magnitude slower than mutex... 

>> Programmers may need do it without
>> dynamic memory allocation, unconstrained types, tasking, exceptions
>> whatever. Remove them from the language and anything else they may need go
>> without. Then we'll talk.
> 
> Programmers do work in such restricted environments,
> for the most part, when using SPARK. Ravenscar was
> made to be more efficient than full Ada tasking.
> Ada people talk about this.

Nevertheless all these features are still Ada, according to the RM.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

Re: Safety of unprotected concurrent operations on constant objects

[Simon Wright]

"G.B." <rm-dash-bau-haus@dash.futureapps.de> writes:

> The "sequential checks" that handle tampering already add to Ada
> containers being slow in comparison.

To what?

I did a very simple comparison of the Containers vs the BCs, and the
Containers won (I forget by how much). The BCs don't protect against
tampering.

Re: Safety of unprotected concurrent operations on constant objects

[Georg Bauhaus]

On 07/05/14 19:45, Simon Wright wrote:
> "G.B." <rm-dash-bau-haus@dash.futureapps.de> writes:
>
>> The "sequential checks" that handle tampering already add to Ada
>> containers being slow in comparison.
>
> To what?

GNAT's maps, for example, are slower than GNAT's own hash table
(the one that is not as easy to use as maps).

While Dmitry's "protected new" would be simple to use (if it
will work), I imagine containers that replace the defensive
checks for tampering etc. with contracts. The proof obligations
that follow will mean more work for users, but in return for
following the contract, concurrent reads can be safe and also
a little faster. At least the contract could make Element as
safe as reading array components in parallel.

Re: Safety of unprotected concurrent operations on constant objects

[J-P. Rosen]

Le 06/05/2014 17:00, Dmitry A. Kazakov a écrit :
> I pointed out that manual wrapping of operations is tedious, error prone,
> and the potential damage is incredibly high as bugs may stay undetected in
> the production code for years and there is no way to write a test for such
> bugs.
> 
Note that in your examples, you just considered explicit locks and
assumed lock checking on the caller's side. There are other, safer ways.

For example, in Aegis, the system that manages registrations to the
Ada-Europe conference (plug: http://www.ada-europe.org/conference2014),
we use a (SQLite) database (not exactly the same issues as containers,
but close enough). All requests are encapsulated in a task, whose
(simplified) scheme is:

loop
   accept Begin_Transaction;
   loop
      select
         accept Request;
      or
         accept End_Transaction;
         exit;
      end select;
   end loop;
end loop;

The only constraint on the user is to call Begin_Transaction at the
beginning, and End_Transaction in the end, which is quite acceptable for
database transactions!

Of course, we are in a favourable context: all the transactions are done
within the building of one web page, and concurrent transactions are
unlikely (we have typically 2-5 registrations a day), so delaying a
request by even one tenth of a second is not an issue! YMMV.

-- 
J-P. Rosen
Adalog
2 rue du Docteur Lombard, 92441 Issy-les-Moulineaux CEDEX
Tel: +33 1 45 29 21 52, Fax: +33 1 45 29 25 00
http://www.adalog.fr

Re: Safety of unprotected concurrent operations on constant objects

[Dmitry A. Kazakov]

On Wed, 07 May 2014 06:59:52 +0200, J-P. Rosen wrote:

> Le 06/05/2014 17:00, Dmitry A. Kazakov a écrit :
>> I pointed out that manual wrapping of operations is tedious, error prone,
>> and the potential damage is incredibly high as bugs may stay undetected in
>> the production code for years and there is no way to write a test for such
>> bugs.
>> 
> Note that in your examples, you just considered explicit locks and
> assumed lock checking on the caller's side. There are other, safer ways.

Yes, I specifically said that the implementation would be free to choose
synchronization method, and also mentioned monitor as one. [Your example
uses a monitor]

> The only constraint on the user is to call Begin_Transaction at the
> beginning, and End_Transaction in the end, which is quite acceptable for
> database transactions!

I tend to have a controlled transaction handler, which rolls back upon
finalization [unless there was explicit Commit].

P.S. It would be nice to have a mandated way to detect if Finalize was
called with an exception being propagated. E.g. the pending transaction is
committed in Finalize when there is no exception and rolled back otherwise
There is a way to do this, but it is GNAT-specific.

P.P.S. Monitor is not always safer, not even always possible, because some
clients require a transaction bound to the single task. I.e. you could not
start several transactions in the monitor on behalf of several tasks. On
the other hand a mutex implementation will fail when a transaction started
by one task will be closed by another. A controlled stack-allocated handler
would prevent this, but it is not always possible to have it on the stack.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

Re: Safety of unprotected concurrent operations on constant objects

[J-P. Rosen]

Le 07/05/2014 09:30, Dmitry A. Kazakov a écrit :
>> The only constraint on the user is to call Begin_Transaction at the
>> > beginning, and End_Transaction in the end, which is quite acceptable for
>> > database transactions!
> I tend to have a controlled transaction handler, which rolls back upon
> finalization [unless there was explicit Commit].
Sure, I said it was a simplified view. In practice, Begin/End
transactions are part of a limited_controlled object declared in the
callback procedure  of AWS.

> P.S. It would be nice to have a mandated way to detect if Finalize was
> called with an exception being propagated. E.g. the pending transaction is
> committed in Finalize when there is no exception and rolled back otherwise
> There is a way to do this, but it is GNAT-specific.
Since everything is handled by the task, it is easy to have a local
flag, and when you close the transaction do a rollback unless the
previous order was commit. (not the way we do it in Aegis, but for other
reasons).

> P.P.S. Monitor is not always safer, not even always possible, because some
> clients require a transaction bound to the single task. I.e. you could not
> start several transactions in the monitor on behalf of several tasks.
I don't understand your remark here. It is precisely because SQLite did
not seem to be able to handle transactions from several tasks
(concurrent or not) that I delegated all the DB interface to a single
task. This serializes all requests, but it is no big deal in our case,
since a transaction is never longer than the time to build a web page.

-- 
J-P. Rosen
Adalog
2 rue du Docteur Lombard, 92441 Issy-les-Moulineaux CEDEX
Tel: +33 1 45 29 21 52, Fax: +33 1 45 29 25 00
http://www.adalog.fr

Re: Safety of unprotected concurrent operations on constant objects

[Dmitry A. Kazakov]

On Wed, 07 May 2014 10:26:41 +0200, J-P. Rosen wrote:

> Le 07/05/2014 09:30, Dmitry A. Kazakov a écrit :
>>> The only constraint on the user is to call Begin_Transaction at the
>>> > beginning, and End_Transaction in the end, which is quite acceptable for
>>> > database transactions!
>> I tend to have a controlled transaction handler, which rolls back upon
>> finalization [unless there was explicit Commit].
> Sure, I said it was a simplified view. In practice, Begin/End
> transactions are part of a limited_controlled object declared in the
> callback procedure  of AWS.
> 
>> P.S. It would be nice to have a mandated way to detect if Finalize was
>> called with an exception being propagated. E.g. the pending transaction is
>> committed in Finalize when there is no exception and rolled back otherwise
>> There is a way to do this, but it is GNAT-specific.
> Since everything is handled by the task, it is easy to have a local
> flag, and when you close the transaction do a rollback unless the
> previous order was commit.

This how I do it too. The point is to do this safer, without a need to
commit explicitly, which could be easily forgotten or misplaced (done
before last requests). When you leave the scope, the changes are committed.
If you leave the scope by a DB request or other error (manifested as an
exception), it is rolled back.

>> P.P.S. Monitor is not always safer, not even always possible, because some
>> clients require a transaction bound to the single task. I.e. you could not
>> start several transactions in the monitor on behalf of several tasks.
> I don't understand your remark here. It is precisely because SQLite did
> not seem to be able to handle transactions from several tasks
> (concurrent or not) that I delegated all the DB interface to a single
> task. This serializes all requests, but it is no big deal in our case,
> since a transaction is never longer than the time to build a web page.

Yes, but for a DBMS capable of handling multiple transactions, it would
become a bottleneck.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

Re: Safety of unprotected concurrent operations on constant objects

[J-P. Rosen]

Le 07/05/2014 11:09, Dmitry A. Kazakov a écrit :
>> Since everything is handled by the task, it is easy to have a local
>> > flag, and when you close the transaction do a rollback unless the
>> > previous order was commit.
> This how I do it too. The point is to do this safer, without a need to
> commit explicitly, which could be easily forgotten or misplaced (done
> before last requests). When you leave the scope, the changes are committed.
> If you leave the scope by a DB request or other error (manifested as an
> exception), it is rolled back.
Well, if in addition Begin/End of transactions are from
Initialize/Finalize of a controlled objet, you are safe.

>>> >> P.P.S. Monitor is not always safer, not even always possible, because some
>>> >> clients require a transaction bound to the single task. I.e. you could not
>>> >> start several transactions in the monitor on behalf of several tasks.
>> > I don't understand your remark here. It is precisely because SQLite did
>> > not seem to be able to handle transactions from several tasks
>> > (concurrent or not) that I delegated all the DB interface to a single
>> > task. This serializes all requests, but it is no big deal in our case,
>> > since a transaction is never longer than the time to build a web page.
> Yes, but for a DBMS capable of handling multiple transactions, it would
> become a bottleneck.
Which SQLite is not, unfortunately, and despite what they seem to tell.

In our case, we have less than 1% chance of having two transactions at
the same time, so the bottleneck is not an issue (as long as we don't
ruin the database, which IS important). Other contexts may be different,
of course.

-- 
J-P. Rosen
Adalog
2 rue du Docteur Lombard, 92441 Issy-les-Moulineaux CEDEX
Tel: +33 1 45 29 21 52, Fax: +33 1 45 29 25 00
http://www.adalog.fr

Re: Safety of unprotected concurrent operations on constant objects (was: Safety of unprotected concurrent operations on constant objects)

[Dmitry A. Kazakov]

On Wed, 07 May 2014 13:29:24 +0200, J-P. Rosen wrote:

> Which SQLite is not, unfortunately, and despite what they seem to tell.

It is difficult to do with single file, I suppose. If the DB is single-file
and transactions are safe, in the sense that if you turn the power off when
a transaction is pending (the file is being written), the effect is like
rolling all updates back. Then multiple transactions is a hardball.

I toyed with an idea of making a safe equivalent of Ada's Direct_IO. Even
with single transaction it would be very challenging. My idea, roughly, was
to map file blocks: virtual -> physical. When a virtual block gets updated
a new physical is allocated or reused and the mapping is adjusted. When the
transaction is committed the mapping is stored in the file check-summed
etc. Old blocks are reused upon next transaction. This would be a
single-transaction schema.
 
> In our case, we have less than 1% chance of having two transactions at
> the same time, so the bottleneck is not an issue (as long as we don't
> ruin the database, which IS important). Other contexts may be different,
> of course.

I think a better case for synchronization  monitor would be GUI (when based
on a messages loop). Windows GDI is task-safe because it sends messages to
the loop. This is a monitor already. I don't understand why GTK (under
Linux) tried to use locks instead of marshaling messages. It does not make
sense to me.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

Re: Safety of unprotected concurrent operations on constant objects

[G.B.]

On 06.05.14 10:11, Dmitry A. Kazakov wrote:
> If you limit it to primitive operations then much simpler to do this:
>
>     type My_Container is tagged ...; -- All operations are unsafe
>
>     type My_Safe_Container is protected new My_Container with null record;
>
> When inherited from, the compiler would override each primitive operation
> and wrap it with a reentrant mutex taken. When an operation gets overridden
> its new body is wrapped. Calling operation within a protected action would
> be bounded error. At least the compiler would be able to maintain mutexes
> of such objects, e.g. order them to prevent deadlocks.

Incidentally, "protected new" is like what was planned for
the "separate" keyword of Eiffel, which stands for "separate
processor". So far, the outcome seems to be that after some
20 years, they have had to severely restrict the language,
in order to facilitate some intensely formal analysis of the
possibilities, and pitfalls.


class SQNTL          | separate class SQNTL
feature              | feature
    foo               |    foo
      require ...     |      require ...
      ensure ...      |      ensure ...
end                  |  end

The idea being that DbC would work in concurrent programs
in ways similar to how it works in sequential programs.

Re: Safety of unprotected concurrent operations on constant objects

[Brad Moore]

On 06/05/2014 2:11 AM, Dmitry A. Kazakov wrote:
> On Tue, 06 May 2014 00:00:40 -0600, Brad Moore wrote:
>
>> On 05/05/2014 10:36 AM, Dmitry A. Kazakov wrote:
>>> On Mon, 05 May 2014 09:11:05 -0600, Brad Moore wrote:
>>>
>>>> Eg. For Ada.Containers.Vectors...
>>>>
>>>> type Vector is tagged private
>>>>       with
>>>>          Constant_Indexing => Constant_Reference,
>>>>          Variable_Indexing => Reference,
>>>>          Default_Iterator  => Iterate,
>>>>          Iterator_Element  => Element_Type,
>>>>          Task_Safe         => False;
>>>>
>>>> Then programmers could apply the aspect to their own abstractions, which
>>>> better defines the contract of the subprogram or type.
>>>
>>> Task safety is not a type property. Even for a tagged type an unsafe
>>> operation can be defined later on. For non-tagged types it is even less
>>> clear which operations must be safe and which not.
>>>
>>> Furthermore, task-safety cannot be inherited or composed. At least not
>>> without massive overhead to prevent deadlocking when two safe types meet as
>>> mutable parameters of a safe subprogram.
>>
>> I agree that such a property is not likely inheritable or composable,
>> and I don't think we'd want it to be.  I think conceivably it could
>> apply to a type, however. It may be that such an aspect could only be
>> applicable to tagged types, and only would apply to the primitive
>> subprograms of that type. The aspect, if true would become false for any
>> derivations of that type, unless those derived types also explicitly set
>> the aspect to True.
>
> If you limit it to primitive operations then much simpler to do this:
>
>     type My_Container is tagged ...; -- All operations are unsafe
>
>     type My_Safe_Container is protected new My_Container with null record;

There's quite a difference from what you propose and what I was 
suggesting. In a nutshell, your idea is to *prescribe* an implementation 
(by wrapping an existing implementation in mutexes, whereas my wish is 
to be better able to *describe* an implementation.
There are lots of ways to provide a task safe implementation, and lots 
of different flavours of task-safe it seems.

Also, the main driver behind what I was suggesting was not to apply the 
aspect to a type, but rather to apply it to a subprogram specification. 
Any subprogram specification, whether its a primitive of a tagged type 
or not.

I only suggested applying the aspect to the primitives of a tagged type, 
as an extension to the idea, as a shorthand for putting the same aspect 
on every primitive subprogram. That part of the idea could be dropped if 
it is too problematic. When the aspect is applied to a type rather than 
a subprogram, I suspect that it would be problematic to apply to 
non-tagged types. If you imagine a function that takes a parameter of a 
task safe type, and another of a non-task safe type type, would the 
function be task safe or not? It seems
clearer that the aspect could work on a tagged type, and only apply to 
the primitives of the tagged type.

As a better example of my main concern, consider the following function.

     type Foo_Range is range 1 .. 1000;

     function Foo (X : Foo_Range) return Integer;

Looking at this, can someone tell me if the function is task-safe or 
not? Who knows? The function might internally use X to update some 
unprotected global statistic variable recording the max, min, and 
average values of all calls for the value of X.

Calling Foo with any combination of arguments concurrently for such a 
case would be dangerous, regardless the values of X.

Now consider that Foo instead uses X as an index to update the value in
some global unprotected array.

In this case, calling Foo from multiple tasks is task-safe, so long as 
two tasks do not call Foo concurrently with the same values of X.

Finally, the function may be task-safe, declaring any state on the stack 
without updating any global variables.

Whether or not such a function can be called concurrently is a pretty 
basic question, but Ada currently doesn't help the reader here.

If you are quite lucky, the programmer might have specified this
in the comments associated with the function. If you are unlucky, the 
programmer didn't later modify the implementation to become task 
un-safe, but neglected to update the comment.

Now that Ada has the new contract capabilities in Ada 2012, it seems 
like a large hole that there is no way to specify the task safety in the 
contract as well, so I am wondering about what can be done to improve 
that situation.

In response to your protected new suggestion. I think there is an idea 
there that could be explored, but I suspect there could be significant 
difficulties in having such an auto-generated protection scheme added to 
Ada. When it comes to task-safety, one size does not fit all.

For example, someone interested in processing a Vector container in 
parallel would likely not want to use such a feature, because it applies 
a mutex to every access to the container, when a much more efficient 
implementation would break the index range into chunks, and
a group of worker tasks could process each chunk of the array without 
any synchronization.

In other cases, moving from a single task design to a multiple task 
design changes the design. A producer/consumer type of usage for a 
bounded container would likely want blocking introduced to calls when 
the container is full, or empty. Simply putting a mutex around all the 
calls is not the best design in that case.

A worry I'd have is that such a feature might encourage programmers to 
become lazy and start writing poorer abstractions in lieu of taking the 
time to write a better one, in respect to functionality, readability, 
safety, etc.

>
> When inherited from, the compiler would override each primitive operation
> and wrap it with a reentrant mutex taken. When an operation gets overridden
> its new body is wrapped. Calling operation within a protected action would
> be bounded error. At least the compiler would be able to maintain mutexes
> of such objects, e.g. order them to prevent deadlocks.
>
> [Better of course, would be to have a decent delegation support]
>
>>> And, just how this contract is supposed to be verified?
>>
>> I see it more as a contract or promise made by the implementer to the
>> users of that subprogram that concurrent calls to the subprogram will
>> work.
>
> You can use this contract no more you can verify it. Because the compiler
> does not know if a call is concurrent or not.
>
>> At this point, I have doubts that the compiler could 100% guarantee that
>> a subprogram call is task safe, but there are likely rules and
>> restrictions that could be applied that would allow the compiler to
>> catch many problems.
>>
>> In particular, the aspect could restrict the associated subprogram to
>> disallow:
>>
>> (1) Calls on other non-protected subprograms that are not Pure or
>>       Task_Safe;
>
> But calling a task-safe subprogram from another task-safe subprogram were a
> much bigger problem than calling a non-safe subprogram. Protected
> operations specifically forbid to do exactly this.

That's not correct. Protected procedure's and protected functions are 
not potentially blocking. A protected procedure of one PO can call 
another protected procedure of another PO.

You could call another
> task-safe operation only on the same object and only if the implementation
> deploys reentrant locking.



>
> The rules you propose actually are good only for lock-free concurrency.

There's million's of simple functions and procedures that do not involve 
any locking. Integer "+" for example, is completely task safe.

> Unfortunately only few things can be done lock-free, and most types of
> containers certainly not.
>

Containers maybe not in general, but a constant container object without 
tamper checks could easily be made to be task safe, for functions that 
query the container, as per the original OP's request.

Regards, Brad

Re: Safety of unprotected concurrent operations on constant objects

[Dmitry A. Kazakov]

On Wed, 07 May 2014 22:12:13 -0600, Brad Moore wrote:

> On 06/05/2014 2:11 AM, Dmitry A. Kazakov wrote:
>> On Tue, 06 May 2014 00:00:40 -0600, Brad Moore wrote:
>>
>>> On 05/05/2014 10:36 AM, Dmitry A. Kazakov wrote:
>>>> On Mon, 05 May 2014 09:11:05 -0600, Brad Moore wrote:
>>>>
>>>>> Eg. For Ada.Containers.Vectors...
>>>>>
>>>>> type Vector is tagged private
>>>>>       with
>>>>>          Constant_Indexing => Constant_Reference,
>>>>>          Variable_Indexing => Reference,
>>>>>          Default_Iterator  => Iterate,
>>>>>          Iterator_Element  => Element_Type,
>>>>>          Task_Safe         => False;
>>>>>
>>>>> Then programmers could apply the aspect to their own abstractions, which
>>>>> better defines the contract of the subprogram or type.
>>>>
>>>> Task safety is not a type property. Even for a tagged type an unsafe
>>>> operation can be defined later on. For non-tagged types it is even less
>>>> clear which operations must be safe and which not.
>>>>
>>>> Furthermore, task-safety cannot be inherited or composed. At least not
>>>> without massive overhead to prevent deadlocking when two safe types meet as
>>>> mutable parameters of a safe subprogram.
>>>
>>> I agree that such a property is not likely inheritable or composable,
>>> and I don't think we'd want it to be.  I think conceivably it could
>>> apply to a type, however. It may be that such an aspect could only be
>>> applicable to tagged types, and only would apply to the primitive
>>> subprograms of that type. The aspect, if true would become false for any
>>> derivations of that type, unless those derived types also explicitly set
>>> the aspect to True.
>>
>> If you limit it to primitive operations then much simpler to do this:
>>
>>     type My_Container is tagged ...; -- All operations are unsafe
>>
>>     type My_Safe_Container is protected new My_Container with null record;
> 
> There's quite a difference from what you propose and what I was 
> suggesting. In a nutshell, your idea is to *prescribe* an implementation 
> (by wrapping an existing implementation in mutexes, whereas my wish is 
> to be better able to *describe* an implementation.

To me description that does not prescribe is a lie.

> Now that Ada has the new contract capabilities in Ada 2012,

You know what I think about these...

> it seems 
> like a large hole that there is no way to specify the task safety in the 
> contract as well, so I am wondering about what can be done to improve 
> that situation.

From the program correctness POV, yes, it is fine to provide some axioms
for the prover which would use them.

But this is not the case here. In fact, proving "safety" of an operation is
easier than proving safety of a combination of "safe" operations.

And you are not going to prove it to hold, as a contract must do. Not even
to check it at run-time, to annoy the programmer, as Ada 2012 "contracts"
do.

> For example, someone interested in processing a Vector container in 
> parallel would likely not want to use such a feature, because it applies 
> a mutex to every access to the container, when a much more efficient 
> implementation would break the index range into chunks, and
> a group of worker tasks could process each chunk of the array without 
> any synchronization.

Right, that is a common method, with read-write mutexes used.

Though note, this as well applies to the container library in general. In
such an application you would not use standard library Vector anyway.
Because fine-grained locking would not work, while more coarse and
efficient locking will require interaction with the container inner
architecture and outer interface.

If you accept language-provided containers without much consideration, you
can also accept the proposed way to make them kind of safe.

> A worry I'd have is that such a feature might encourage programmers to 
> become lazy and start writing poorer abstractions in lieu of taking the 
> time to write a better one, in respect to functionality, readability, 
> safety, etc.

Yes. As I said, I would prefer delegation support over a specific case of
compiler-generated wrappers.

>>> In particular, the aspect could restrict the associated subprogram to
>>> disallow:
>>>
>>> (1) Calls on other non-protected subprograms that are not Pure or
>>>       Task_Safe;
>>
>> But calling a task-safe subprogram from another task-safe subprogram were a
>> much bigger problem than calling a non-safe subprogram. Protected
>> operations specifically forbid to do exactly this.
> 
> That's not correct. Protected procedure's and protected functions are 
> not potentially blocking. A protected procedure of one PO can call 
> another protected procedure of another PO.

I meant 9.5.1 (15). The rationale to have it, IMO, was to ease
implementations not to care about deadlocks upon locking multiple mutexes. 

Same problems will arise when composing task-safe operations. Surely there
are means to prevent deadlocking whenever the synchronization is done per
mutexes or per monitors, but these means are not for free.

>> The rules you propose actually are good only for lock-free concurrency.
> 
> There's million's of simple functions and procedures that do not involve 
> any locking. Integer "+" for example, is completely task safe.

Maybe yes, maybe no. E.g. purely theoretically, consider 64-bit integer "+"
on i686 in 32-bit mode. The implementation could use movq instruction and
alike which in turn would have effect on the FPU (turning it off). It will
restore FPU state upon return, but that would make it unsafe.

In other subthread Randy provided a real-life story for integer "/".

>> Unfortunately only few things can be done lock-free, and most types of
>> containers certainly not.
> 
> Containers maybe not in general, but a constant container object without 
> tamper checks could easily be made to be task safe, for functions that 
> query the container, as per the original OP's request.

Yes, but this a very rare scenario (static container), which does not
deserve special treatment.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

Re: Safety of unprotected concurrent operations on constant objects

[G.B.]

On 08.05.14 10:20, Dmitry A. Kazakov wrote:
>> Containers maybe not in general, but a constant container object without
>> >tamper checks could easily be made to be task safe, for functions that
>> >query the container, as per the original OP's request.
> Yes, but this a very rare scenario (static container), which does not
> deserve special treatment.

Constant (non-static) views of containers abound, in particular
with big-data---data items being small or big. In fact, every
database-like structure frequently has two modes:

- reading, in order to gain insight (for filtering,  statistics,
   decision support ...),

- writing, updating the facts, adding "history", ...

Imagine some internet appliance, of which there are millions.
The better ones will have specialized processors. Each of them
will need access to the data, some for reading, some for writing.
How about each of them then relying on both the efficiency and
the task safety of tables (and associated interface)?

I think that scenarios like this might deserve special treatment.

I also imagine that image processing might use shared arrays,
though perhaps unbounded. They would become constant as soon as
all image data have been acquired and stored in them, ready
for inspection, or as input to later stages.

Maybe a scenario like this might deserve special treatment, too.

Re: Safety of unprotected concurrent operations on constant objects

[Brad Moore]

On 08/05/2014 2:20 AM, Dmitry A. Kazakov wrote:
> On Wed, 07 May 2014 22:12:13 -0600, Brad Moore wrote:
>
>> On 06/05/2014 2:11 AM, Dmitry A. Kazakov wrote:
>>> On Tue, 06 May 2014 00:00:40 -0600, Brad Moore wrote:
>>>
>>>> On 05/05/2014 10:36 AM, Dmitry A. Kazakov wrote:
>>>>> On Mon, 05 May 2014 09:11:05 -0600, Brad Moore wrote:
>>>>>
>>>>>> Eg. For Ada.Containers.Vectors...
>>>>>>
>>>>>> type Vector is tagged private
>>>>>>        with
>>>>>>           Constant_Indexing => Constant_Reference,
>>>>>>           Variable_Indexing => Reference,
>>>>>>           Default_Iterator  => Iterate,
>>>>>>           Iterator_Element  => Element_Type,
>>>>>>           Task_Safe         => False;
>>>>>>
>>>>>> Then programmers could apply the aspect to their own abstractions, which
>>>>>> better defines the contract of the subprogram or type.
>>>>>
>>>>> Task safety is not a type property. Even for a tagged type an unsafe
>>>>> operation can be defined later on. For non-tagged types it is even less
>>>>> clear which operations must be safe and which not.
>>>>>
>>>>> Furthermore, task-safety cannot be inherited or composed. At least not
>>>>> without massive overhead to prevent deadlocking when two safe types meet as
>>>>> mutable parameters of a safe subprogram.
>>>>
>>>> I agree that such a property is not likely inheritable or composable,
>>>> and I don't think we'd want it to be.  I think conceivably it could
>>>> apply to a type, however. It may be that such an aspect could only be
>>>> applicable to tagged types, and only would apply to the primitive
>>>> subprograms of that type. The aspect, if true would become false for any
>>>> derivations of that type, unless those derived types also explicitly set
>>>> the aspect to True.
>>>
>>> If you limit it to primitive operations then much simpler to do this:
>>>
>>>      type My_Container is tagged ...; -- All operations are unsafe
>>>
>>>      type My_Safe_Container is protected new My_Container with null record;
>>
>> There's quite a difference from what you propose and what I was
>> suggesting. In a nutshell, your idea is to *prescribe* an implementation
>> (by wrapping an existing implementation in mutexes, whereas my wish is
>> to be better able to *describe* an implementation.
>
> To me description that does not prescribe is a lie.

It is true that the Task_Safe aspect would be prescribing some 
restrictions that are meant to enforce the intent as best as possible, 
but it also documents the intent of the programmer. So to be more 
precise, the Task_Safe mechanism doesn't prescribe a specific 
implementation for the programmer. It only prescribes that whatever 
implementation the programmer chooses, it should be task safe.

The "new protected" feature you described, if it were implemented would 
be one possible implementation the programmer could choose, of many.

>
>> Now that Ada has the new contract capabilities in Ada 2012,
>
> You know what I think about these...
>

I take it that you're not a fan of these, but I think there are lots of 
fans out there. In that regard, it's good that contracts aren't mandatory.
If you don't like them, you don't have to use them.


>> it seems
>> like a large hole that there is no way to specify the task safety in the
>> contract as well, so I am wondering about what can be done to improve
>> that situation.
>
>  From the program correctness POV, yes, it is fine to provide some axioms
> for the prover which would use them.

Not just for provers, but also for human readers of the source code. It 
conveys the intent of the programmer to the reader, which might be 
another programmer who wants to use that abstraction.

>
> But this is not the case here. In fact, proving "safety" of an operation is
> easier than proving safety of a combination of "safe" operations.
>
> And you are not going to prove it to hold, as a contract must do. Not even
> to check it at run-time, to annoy the programmer, as Ada 2012 "contracts"
> do.

I think it could be a static check, done at compile time, so it'd be 
similar to a Static_Predicate check, which is another form of contract.
And like a type invariant, which is another form of contract, it doesn't 
"prove" that the invariant can never be false, but it would do
a reasonable amount of checking to catch hopefully most problems, and it
captures the intent of the programmer.

>
>> For example, someone interested in processing a Vector container in
>> parallel would likely not want to use such a feature, because it applies
>> a mutex to every access to the container, when a much more efficient
>> implementation would break the index range into chunks, and
>> a group of worker tasks could process each chunk of the array without
>> any synchronization.
>
> Right, that is a common method, with read-write mutexes used.
>
> Though note, this as well applies to the container library in general. In
> such an application you would not use standard library Vector anyway.
> Because fine-grained locking would not work, while more coarse and
> efficient locking will require interaction with the container inner
> architecture and outer interface.
>
> If you accept language-provided containers without much consideration, you
> can also accept the proposed way to make them kind of safe.
>
>> A worry I'd have is that such a feature might encourage programmers to
>> become lazy and start writing poorer abstractions in lieu of taking the
>> time to write a better one, in respect to functionality, readability,
>> safety, etc.
>
> Yes. As I said, I would prefer delegation support over a specific case of
> compiler-generated wrappers.

Probably an idea that should be explored...

>
>>>> In particular, the aspect could restrict the associated subprogram to
>>>> disallow:
>>>>
>>>> (1) Calls on other non-protected subprograms that are not Pure or
>>>>        Task_Safe;
>>>
>>> But calling a task-safe subprogram from another task-safe subprogram were a
>>> much bigger problem than calling a non-safe subprogram. Protected
>>> operations specifically forbid to do exactly this.
>>
>> That's not correct. Protected procedure's and protected functions are
>> not potentially blocking. A protected procedure of one PO can call
>> another protected procedure of another PO.
>
> I meant 9.5.1 (15). The rationale to have it, IMO, was to ease
> implementations not to care about deadlocks upon locking multiple mutexes.
>
> Same problems will arise when composing task-safe operations. Surely there
> are means to prevent deadlocking whenever the synchronization is done per
> mutexes or per monitors, but these means are not for free.
>
>>> The rules you propose actually are good only for lock-free concurrency.
>>
>> There's million's of simple functions and procedures that do not involve
>> any locking. Integer "+" for example, is completely task safe.
>
> Maybe yes, maybe no. E.g. purely theoretically, consider 64-bit integer "+"
> on i686 in 32-bit mode. The implementation could use movq instruction and
> alike which in turn would have effect on the FPU (turning it off). It will
> restore FPU state upon return, but that would make it unsafe.
>
> In other subthread Randy provided a real-life story for integer "/".
>
>>> Unfortunately only few things can be done lock-free, and most types of
>>> containers certainly not.
>>
>> Containers maybe not in general, but a constant container object without
>> tamper checks could easily be made to be task safe, for functions that
>> query the container, as per the original OP's request.
>
> Yes, but this a very rare scenario (static container), which does not
> deserve special treatment.
>

Re: Safety of unprotected concurrent operations on constant objects

[Dmitry A. Kazakov]

On Fri, 09 May 2014 07:14:09 -0600, Brad Moore wrote:

> On 08/05/2014 2:20 AM, Dmitry A. Kazakov wrote:

>> To me description that does not prescribe is a lie.
> 
> It is true that the Task_Safe aspect would be prescribing some 
> restrictions that are meant to enforce the intent as best as possible, 
> but it also documents the intent of the programmer. So to be more 
> precise, the Task_Safe mechanism doesn't prescribe a specific 
> implementation for the programmer. It only prescribes that whatever 
> implementation the programmer chooses, it should be task safe.

In other words is a comment. I prefer old -- -style comments.

>>> it seems
>>> like a large hole that there is no way to specify the task safety in the
>>> contract as well, so I am wondering about what can be done to improve
>>> that situation.
>>
>>  From the program correctness POV, yes, it is fine to provide some axioms
>> for the prover which would use them.
> 
> Not just for provers, but also for human readers of the source code. It 
> conveys the intent of the programmer to the reader, which might be 
> another programmer who wants to use that abstraction.

No. It is not the intent. Intent to me is about program semantics, the
meaning of the program, what the program is supposed to do. Safety or
unsafety is a usage constraint, how you should use the program in order to
retain its meaning. Safety is a constraint which, differently to
preconditions, interfaces, types of entities etc, has a nasty nature that
makes it impossible to spell in a language of Turing-complete power.

>> But this is not the case here. In fact, proving "safety" of an operation is
>> easier than proving safety of a combination of "safe" operations.
>>
>> And you are not going to prove it to hold, as a contract must do. Not even
>> to check it at run-time, to annoy the programmer, as Ada 2012 "contracts"
>> do.
> 
> I think it could be a static check, done at compile time, so it'd be 
> similar to a Static_Predicate check, which is another form of contract.
> And like a type invariant, which is another form of contract, it doesn't 
> "prove" that the invariant can never be false, but it would do
> a reasonable amount of checking to catch hopefully most problems, and it
> captures the intent of the programmer.

No.

Ada 2012 "dynamic invariant" (which is not an invariant, but an arbitrary
expression) is *computable*.

Invariant proper is *provable*.

Task safety is neither computable nor provable. The only way of ensuring
task safety is per construction, when you would prove, usually using more
powerful apparatus than machine prover (i.e. with pen and paper) that given
method of construction yields safety under specified conditions. 

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

Re: Safety of unprotected concurrent operations on constant objects

[Brad Moore]

On 09/05/2014 1:00 PM, Dmitry A. Kazakov wrote:
> On Fri, 09 May 2014 07:14:09 -0600, Brad Moore wrote:
>
>> On 08/05/2014 2:20 AM, Dmitry A. Kazakov wrote:
>
>>> To me description that does not prescribe is a lie.
>>
>> It is true that the Task_Safe aspect would be prescribing some
>> restrictions that are meant to enforce the intent as best as possible,
>> but it also documents the intent of the programmer. So to be more
>> precise, the Task_Safe mechanism doesn't prescribe a specific
>> implementation for the programmer. It only prescribes that whatever
>> implementation the programmer chooses, it should be task safe.
>
> In other words is a comment. I prefer old -- -style comments.
>

It'd be far, far better than a comment, in my mind. A comment doesn't 
cause compilations to fail. A comment does not improve the safety of a 
program, only the quality of the code in the sense that uncommented code 
tends to be harder to read and understand.

While it goes too far to say that the Task_Safe aspect would prove task 
safety, it would prove that the subprogram does not refer to any 
unprotected, non-atomic variables in a global scope. It also proves that 
the subprogram does not call any other subprograms that do the same. 
That goes a long way on the task safe spectrum

If Foo calls Bar, and both Foo and Bar have the Task_Safe aspect, but 
some time later the maintainer of Bar decides to change its 
implementation to refer to some global variable or call some other 
subprogram that doesn't have the Task_Safe aspect, the compiler would 
force the programmer to remove the Task_Safe aspect from Bar. This would 
have a ripple effect, so that a program that calls Foo would fail 
compilation, and force the maintainer of Foo to remove the Task_Safe 
aspect on that subprogram. The maintainer of Bar would realize that he 
is breaking its contract, and might decide to revert his change, or 
choose a different implementation that allows him to leave Bar's 
contract intact. With comments, this would have been a maintenance 
hazard. It's not always obvious to a programmer when such a change is 
made, that it breaks such assumptions in the client usage of the 
subprogram. It's also error prone to expect the programmer to 
exhaustively examine all client usage of that subprogram to check for 
such assumptions that might have been broken.

The maintainer of Bar might also not be aware that some of the 
subprograms that Bar calls have dependencies on global variables.
The maintainer of Bar should not have to recursively look at the 
implementation of every subprogram it calls, and every subprogram those 
subprograms call to see if there are unsafe dependencies on unprotected 
global variables.

Further, these aspects (Task_Safe, and Potentially_Blocking) would
improve the safety of other parts of the standard.

The compiler could be used in a stricter rules checking mode that 
forbids protected subprograms or entries from calling subprograms that 
are not Task_Safe, or that are Potentially_Blocking. (At the very least, 
the compiler could issue warnings)

Rather than only relying on a run time check to raise an exception when 
a protected subprogram or entry calls a subprogram that blocks (possibly 
only in rare circumstances that might be missed during testing), it is 
much more likely that the problem would have been caught during compile 
time.

Also, since the compiler cannot prove that calls to other languages such 
as C are not referring to variables unsafely, the Task_Safe aspect would 
likely forbid calls to other languages. A Task_Safe subprogram is one 
written in pure Ada. Some would argue that that alone says a lot about 
the safety quality of the subprogram.

Brad

>>>> it seems
>>>> like a large hole that there is no way to specify the task safety in the
>>>> contract as well, so I am wondering about what can be done to improve
>>>> that situation.
>>>
>>>   From the program correctness POV, yes, it is fine to provide some axioms
>>> for the prover which would use them.
>>
>> Not just for provers, but also for human readers of the source code. It
>> conveys the intent of the programmer to the reader, which might be
>> another programmer who wants to use that abstraction.
>
> No. It is not the intent. Intent to me is about program semantics, the
> meaning of the program, what the program is supposed to do. Safety or
> unsafety is a usage constraint, how you should use the program in order to
> retain its meaning. Safety is a constraint which, differently to
> preconditions, interfaces, types of entities etc, has a nasty nature that
> makes it impossible to spell in a language of Turing-complete power.
>
>>> But this is not the case here. In fact, proving "safety" of an operation is
>>> easier than proving safety of a combination of "safe" operations.
>>>
>>> And you are not going to prove it to hold, as a contract must do. Not even
>>> to check it at run-time, to annoy the programmer, as Ada 2012 "contracts"
>>> do.
>>
>> I think it could be a static check, done at compile time, so it'd be
>> similar to a Static_Predicate check, which is another form of contract.
>> And like a type invariant, which is another form of contract, it doesn't
>> "prove" that the invariant can never be false, but it would do
>> a reasonable amount of checking to catch hopefully most problems, and it
>> captures the intent of the programmer.
>
> No.
>
> Ada 2012 "dynamic invariant" (which is not an invariant, but an arbitrary
> expression) is *computable*.
>
> Invariant proper is *provable*.
>
> Task safety is neither computable nor provable. The only way of ensuring
> task safety is per construction, when you would prove, usually using more
> powerful apparatus than machine prover (i.e. with pen and paper) that given
> method of construction yields safety under specified conditions.
>

Re: Safety of unprotected concurrent operations on constant objects

[Dmitry A. Kazakov]

On Sat, 10 May 2014 06:30:14 -0600, Brad Moore wrote:

> On 09/05/2014 1:00 PM, Dmitry A. Kazakov wrote:
>> On Fri, 09 May 2014 07:14:09 -0600, Brad Moore wrote:
>>
>>> On 08/05/2014 2:20 AM, Dmitry A. Kazakov wrote:
>>
>>>> To me description that does not prescribe is a lie.
>>>
>>> It is true that the Task_Safe aspect would be prescribing some
>>> restrictions that are meant to enforce the intent as best as possible,
>>> but it also documents the intent of the programmer. So to be more
>>> precise, the Task_Safe mechanism doesn't prescribe a specific
>>> implementation for the programmer. It only prescribes that whatever
>>> implementation the programmer chooses, it should be task safe.
>>
>> In other words is a comment. I prefer old -- -style comments.
> 
> It'd be far, far better than a comment, in my mind. A comment doesn't 
> cause compilations to fail.

Neither the aspect should, because, as I said, neither task-safety nor
unsafety follows from safety of called operations.

> If Foo calls Bar, and both Foo and Bar have the Task_Safe aspect, but 
> some time later the maintainer of Bar decides to change its 
> implementation to refer to some global variable or call some other 
> subprogram that doesn't have the Task_Safe aspect, the compiler would 
> force the programmer to remove the Task_Safe aspect from Bar.

But this rule is just wrong. Calling unsafe operation from a safe one will
be pretty much safe in most cases. The reverse is likely wrong.

Compare it with protected actions. It is safe to call an operation which
itself is not protected from a protected operation on the context of a
protected action.

There is no reasonable rules to verify. Safety of an operation is *not*
related to the safety of called operations, not transitive nor
antitransitive.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

Re: Safety of unprotected concurrent operations on constant objects

[Brad Moore]

On 10/05/2014 2:27 PM, Dmitry A. Kazakov wrote:
>> If Foo calls Bar, and both Foo and Bar have the Task_Safe aspect, but
>> some time later the maintainer of Bar decides to change its
>> implementation to refer to some global variable or call some other
>> subprogram that doesn't have the Task_Safe aspect, the compiler would
>> force the programmer to remove the Task_Safe aspect from Bar.
>
> But this rule is just wrong. Calling unsafe operation from a safe one will
> be pretty much safe in most cases. The reverse is likely wrong.

This doesn't make sense to me. There should be no such thing as a Safe 
operation that calls unsafe ones. Wouldn't that mean that the operation 
is unsafe (to use concurrently)?

>
> Compare it with protected actions. It is safe to call an operation which
> itself is not protected from a protected operation on the context of a
> protected action.

But thats only true if the operation is only ever called from within 
that same instance of the protected object (Something that could be 
difficult to know without the aspect), and that there is only one 
instance of that protected type of the protected object. Otherwise its 
not safe to call from a protected operation as there could be other 
concurrent calls calling the unsafe operation.

The following program illustrates this. If you run the program with a 
small value of N (specified on the command line), say 100, then chances 
are the program executes correctly to completion. However if you use a 
larger value of N (say 1_000_000, the default), then the program fails,
due to the use of global variables. In Test1, the Unsafe function is 
called directly from multiple tasks.

In Test2, the same Unsafe function is only called from protected 
functions, but it still fails.
.
In both tests, the failures are due to function Unsafe failing its 
Postcondition.

If the Task_Safe attribute existed, the compiler could have issued a 
warning at compile time that the tasks were calling subprograms that 
weren't Task_Safe, and the problems could have been avoided.


with Ada.Text_IO; use Ada.Text_IO;
with Ada.Exceptions; use Ada;
with Ada.Command_Line;

procedure Test_Task_Safety is

    --  Defaults to 1_000_000, but can be specified on command line
    N : constant Natural := (if Command_Line.Argument_Count >= 1 then
                             Natural'Value (Command_Line.Argument (1))
                             else 1_000_000);

    Global_Data : Integer := 0;

    function Unsafe (X : Natural) return Natural
        with Post => Unsafe'Result = X + 1 --,
         --  Task_Safe => False
        ;

    function Unsafe (X : Natural) return Natural is
    begin
       Global_Data := X;
       Global_Data := Global_Data + 1;
       return Global_Data;
    end Unsafe;

begin

    New_Line;
    Put_Line ("******************************** ");
    Put_Line ("****  Test1 : Unsafe calls ***** ");
    Put_Line ("******************************** ");
    New_Line;

    Test1 : declare

       task type T1 is
       end T1;

       task body T1 is
          Result : Natural := 0;
       begin
          for I in 1 .. N loop
             Result := Unsafe (Result);
          end loop;
          Put_Line ("Result =" & Natural'Image (Result));
       exception
          when E : others =>
             Put_Line ("Task_Died" & 
Ada.Exceptions.Exception_Information (E));
       end T1;

       Workers : array (1 .. 10) of T1;
    begin
       null;
    end Test1;

    New_Line;
    Put_Line ("********************************************************");
    Put_Line ("****  Test2 : Unsafe calls from protected objects ***** ");
    Put_Line ("********************************************************");
    New_Line;

    Test2 : declare

       protected PO1 is
          function Foo (X : Natural) return Natural;
       end PO1;

       protected PO2 is
          function Bar (X : Natural) return Natural;
       end PO2;

       protected body PO1 is
          function Foo (X : Natural) return Natural is
          begin
             return Unsafe (X);
          end Foo;
       end PO1;

       protected body PO2 is
          function Bar (X : Natural) return Natural is
          begin
             return Unsafe (X);
          end Bar;
       end PO2;

       task type T1 is
       end T1;

       task body T1 is
          Result : Natural := 0;
       begin
          for I in 1 .. N loop
             Result := PO1.Foo (Result);
          end loop;
          Put_Line ("Result =" & Natural'Image (Result));
       exception
          when E : others =>
             Put_Line ("Task_Died" & 
Ada.Exceptions.Exception_Information (E));
       end T1;

       task type T2 is
       end T2;

       task body T2 is
          Result : Natural := 0;
       begin
          for I in 1 .. N loop
             Result := PO2.Bar (Result);
          end loop;
          Put_Line ("Result =" & Natural'Image (Result));
       exception
          when E : others =>
             Put_Line ("Task_Died" & 
Ada.Exceptions.Exception_Information (E));
       end T2;

       Foo_Workers : array (1 .. 10) of T1;
       Bar_Workers : array (1 .. 10) of T2;

    begin
       null;
    end Test2;

    null;
end Test_Task_Safety;

Output:

********************************
****  Test1 : Unsafe calls *****
********************************

Task_DiedException name: SYSTEM.ASSERTIONS.ASSERT_FAILURE
Message: failed postcondition from test_task_safety.adb:15

Task_DiedException name: SYSTEM.ASSERTIONS.ASSERT_FAILURE
Message: failed postcondition from test_task_safety.adb:15

Task_DiedException name: SYSTEM.ASSERTIONS.ASSERT_FAILURE
Message: failed postcondition from test_task_safety.adb:15

Task_DiedException name: SYSTEM.ASSERTIONS.ASSERT_FAILURE
Message: failed postcondition from test_task_safety.adb:15

Task_DiedException name: SYSTEM.ASSERTIONS.ASSERT_FAILURE
Message: failed postcondition from test_task_safety.adb:15

Task_DiedException name: SYSTEM.ASSERTIONS.ASSERT_FAILURE
Message: failed postcondition from test_task_safety.adb:15

Task_DiedException name: SYSTEM.ASSERTIONS.ASSERT_FAILURE
Message: failed postcondition from test_task_safety.adb:15

Task_DiedException name: SYSTEM.ASSERTIONS.ASSERT_FAILURE
Message: failed postcondition from test_task_safety.adb:15

Task_DiedException name: SYSTEM.ASSERTIONS.ASSERT_FAILURE
Message: failed postcondition from test_task_safety.adb:15

Result = 1000000

********************************************************
****  Test2 : Unsafe calls from protected objects *****
********************************************************

Task_DiedException name: SYSTEM.ASSERTIONS.ASSERT_FAILURE
Message: failed postcondition from test_task_safety.adb:15

Task_DiedException name: SYSTEM.ASSERTIONS.ASSERT_FAILURE
Message: failed postcondition from test_task_safety.adb:15

Task_DiedException name: SYSTEM.ASSERTIONS.ASSERT_FAILURE
Message: failed postcondition from test_task_safety.adb:15

Task_DiedException name: SYSTEM.ASSERTIONS.ASSERT_FAILURE
Message: failed postcondition from test_task_safety.adb:15

Task_DiedException name: SYSTEM.ASSERTIONS.ASSERT_FAILURE
Message: failed postcondition from test_task_safety.adb:15

Task_DiedException name: SYSTEM.ASSERTIONS.ASSERT_FAILURE
Message: failed postcondition from test_task_safety.adb:15

Task_DiedException name: SYSTEM.ASSERTIONS.ASSERT_FAILURE
Message: failed postcondition from test_task_safety.adb:15

Task_DiedException name: SYSTEM.ASSERTIONS.ASSERT_FAILURE
Message: failed postcondition from test_task_safety.adb:15

Task_DiedException name: SYSTEM.ASSERTIONS.ASSERT_FAILURE
Message: failed postcondition from test_task_safety.adb:15

Task_DiedException name: SYSTEM.ASSERTIONS.ASSERT_FAILURE
Message: failed postcondition from test_task_safety.adb:15

Task_DiedException name: SYSTEM.ASSERTIONS.ASSERT_FAILURE
Message: failed postcondition from test_task_safety.adb:15

Task_DiedException name: SYSTEM.ASSERTIONS.ASSERT_FAILURE
Message: failed postcondition from test_task_safety.adb:15

Task_DiedException name: SYSTEM.ASSERTIONS.ASSERT_FAILURE
Message: failed postcondition from test_task_safety.adb:15

Task_DiedException name: SYSTEM.ASSERTIONS.ASSERT_FAILURE
Message: failed postcondition from test_task_safety.adb:15

Task_DiedException name: SYSTEM.ASSERTIONS.ASSERT_FAILURE
Message: failed postcondition from test_task_safety.adb:15

Task_DiedException name: SYSTEM.ASSERTIONS.ASSERT_FAILURE
Message: failed postcondition from test_task_safety.adb:15

Task_DiedException name: SYSTEM.ASSERTIONS.ASSERT_FAILURE
Message: failed postcondition from test_task_safety.adb:15

Task_DiedException name: SYSTEM.ASSERTIONS.ASSERT_FAILURE
Message: failed postcondition from test_task_safety.adb:15

Task_DiedException name: SYSTEM.ASSERTIONS.ASSERT_FAILURE
Message: failed postcondition from test_task_safety.adb:15

Result = 1000000

Brad
>
> There is no reasonable rules to verify. Safety of an operation is *not*
> related to the safety of called operations, not transitive nor
> antitransitive.
>

Re: Safety of unprotected concurrent operations on constant objects

[Brad Moore]

On 10/05/2014 2:27 PM, Dmitry A. Kazakov wrote:
> On Sat, 10 May 2014 06:30:14 -0600, Brad Moore wrote:
>
>> On 09/05/2014 1:00 PM, Dmitry A. Kazakov wrote:
>>> On Fri, 09 May 2014 07:14:09 -0600, Brad Moore wrote:
>>>
>>>> On 08/05/2014 2:20 AM, Dmitry A. Kazakov wrote:
>>>
>>>>> To me description that does not prescribe is a lie.
>>>>
>>>> It is true that the Task_Safe aspect would be prescribing some
>>>> restrictions that are meant to enforce the intent as best as possible,
>>>> but it also documents the intent of the programmer. So to be more
>>>> precise, the Task_Safe mechanism doesn't prescribe a specific
>>>> implementation for the programmer. It only prescribes that whatever
>>>> implementation the programmer chooses, it should be task safe.
>>>
>>> In other words is a comment. I prefer old -- -style comments.
>>
>> It'd be far, far better than a comment, in my mind. A comment doesn't
>> cause compilations to fail.
>
> Neither the aspect should, because, as I said, neither task-safety nor
> unsafety follows from safety of called operations.
>

> There is no reasonable rules to verify. Safety of an operation is *not*
> related to the safety of called operations, not transitive nor
> antitransitive.
>

A couple more thoughts and refinements to throw in, for consideration.

This got me thinking about what could be done to be able to say with 
more confidence that a Task_Safe subprogram is in fact task safe (i.e 
Safe to call concurrently).

What if we threw in a couple more restrictions.

- A Task_Safe subprogram does not contain any backwards jumping goto 
statements, nor does it contain while loops. (Or at least while loops 
that cannot be easily proven to be guaranteed to exit. For loops however 
are OK, since they are guaranteed to exit)

- A subprogram that does contain backwards jumping goto statements or 
while loops are considered to be potentially blocking, for the purpose 
of the Potentially_Blocking aspect, so applying the Potentially_Blocking 
aspect to such a subprogram would be allowed.

It would be OK for the main body of a task to have while loops of 
course. The compiler would just statically warn about calling 
subprograms that have while loops.

Now it seems to me that when we say Task_Safe, it is more than just 
documenting the intent of the programmer, it is provable.

Such a subprogram for example could not deadlock because it does not 
contain any endless loops, and does not call anything that blocks. It 
also does not refer to any global variables.

With such restrictions, can you provide any example that you would 
consider unsafe? I am having difficulty coming up with one.

Keep in mind also that Task_Safe is not a term defined in the RM. We can 
pretty much define it to mean whatever we want, including something that 
is provable.

Regards,
Brad

Re: Safety of unprotected concurrent operations on constant objects

[Dmitry A. Kazakov]

On Sun, 11 May 2014 12:01:20 -0600, Brad Moore wrote:

> On 10/05/2014 2:27 PM, Dmitry A. Kazakov wrote:
>> On Sat, 10 May 2014 06:30:14 -0600, Brad Moore wrote:
>>
>>> On 09/05/2014 1:00 PM, Dmitry A. Kazakov wrote:
>>>> On Fri, 09 May 2014 07:14:09 -0600, Brad Moore wrote:
>>>>
>>>>> On 08/05/2014 2:20 AM, Dmitry A. Kazakov wrote:
>>>>
>>>>>> To me description that does not prescribe is a lie.
>>>>>
>>>>> It is true that the Task_Safe aspect would be prescribing some
>>>>> restrictions that are meant to enforce the intent as best as possible,
>>>>> but it also documents the intent of the programmer. So to be more
>>>>> precise, the Task_Safe mechanism doesn't prescribe a specific
>>>>> implementation for the programmer. It only prescribes that whatever
>>>>> implementation the programmer chooses, it should be task safe.
>>>>
>>>> In other words is a comment. I prefer old -- -style comments.
>>>
>>> It'd be far, far better than a comment, in my mind. A comment doesn't
>>> cause compilations to fail.
>>
>> Neither the aspect should, because, as I said, neither task-safety nor
>> unsafety follows from safety of called operations.
> 
>> There is no reasonable rules to verify. Safety of an operation is *not*
>> related to the safety of called operations, not transitive nor
>> antitransitive.
> 
> A couple more thoughts and refinements to throw in, for consideration.
> 
> This got me thinking about what could be done to be able to say with 
> more confidence that a Task_Safe subprogram is in fact task safe (i.e 
> Safe to call concurrently).
> 
> What if we threw in a couple more restrictions.
> 
> - A Task_Safe subprogram does not contain any backwards jumping goto 
> statements, nor does it contain while loops. (Or at least while loops 
> that cannot be easily proven to be guaranteed to exit. For loops however 
> are OK, since they are guaranteed to exit)
> 
> - A subprogram that does contain backwards jumping goto statements or 
> while loops are considered to be potentially blocking, for the purpose 
> of the Potentially_Blocking aspect, so applying the Potentially_Blocking 
> aspect to such a subprogram would be allowed.
> 
> It would be OK for the main body of a task to have while loops of 
> course. The compiler would just statically warn about calling 
> subprograms that have while loops.
> 
> Now it seems to me that when we say Task_Safe, it is more than just 
> documenting the intent of the programmer, it is provable.
> 
> Such a subprogram for example could not deadlock because it does not 
> contain any endless loops, and does not call anything that blocks. It 
> also does not refer to any global variables.
> 
> With such restrictions, can you provide any example that you would 
> consider unsafe? I am having difficulty coming up with one.

This looks a useless subprogram to me. As a side note safety is not about
halting or time constraints. A never ending subprogram could be still safe.
Overstretching this a bit, a task body running infinite loop is task-safe.

What I had in mind are designs like:

type T is record
   M : aliased Mutex;
   ...
end record;

A safe operation on this type looks like:

   procedure Safe_Search (X : in out T; ...) is
       Lock : Holder (T.M'Access);
   begin
       Unsafe_Search (X, ...);
   end Safe_Search;

Here safe operations call to unsafe ones all the time and never do each
other because M is not reeentrant.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

Re: Safety of unprotected concurrent operations on constant objects

[Brad Moore]

On 14-05-12 02:13 AM, Dmitry A. Kazakov wrote:
> As a side note safety is not about
> halting or time constraints. A never ending subprogram could be still safe.
> Overstretching this a bit, a task body running infinite loop is task-safe.

Right. And that would still be the case by the rules I have been 
suggesting. (Note the distinction between "task safe" proper and 
Task_Safe the aspect, with an underscore.) The idea is that subprograms 
that have either Task_Safe or Potentially_Blocking aspects are task safe.

I lumped task safe programs with while loops into the 
Potentially_Blocking category, because while loops can be used to 
implement busy spin-loops, which can be considered a form of blocking.


>
> What I had in mind are designs like:
>
> type T is record
>     M : aliased Mutex;
>     ...
> end record;
>
> A safe operation on this type looks like:
>
>     procedure Safe_Search (X : in out T; ...) is
>         Lock : Holder (T.M'Access);
>     begin
>         Unsafe_Search (X, ...);
>     end Safe_Search;
>
> Here safe operations call to unsafe ones all the time and never do each
> other because M is not reeentrant.
>

Thanks for the example. A good case to consider. By the rules I'm 
thinking of, this would not be a task-safe construct however, which I 
think is rightly so.

The Task_Safe attribute is about subprograms that can be proven to be 
safe. This construct is unsafe, because it doesn't guarantee that there 
aren't direct concurrent calls to Unsafe_Search happening while inside 
the body of Safe_Search. (It would probably be too difficult to prove, 
and so its better to assume the worst, when it comes to safety.) 
Therefore Safe_Search is also not a task-safe call.

Another rule I haven't stated is that any subroutine that modifies a 
variable (or internal state) that isn't via a protected object, atomic, 
or volatile and a type that can be atomically updated (such as Integer), 
is not Task_Safe. This would only need to be checked directly in the 
body of the task-safe subprogram, since any subprograms called by that 
subprogram also need to be Task_Safe, and would have been checked during 
their compilation.

So for example, a spinloop on a regular integer would not be considered 
Task_Safe, but a spinloop on a volatile integer would be considered task 
safe (assuming there were no other rule violations).

The rules are meant to be static checks, that are relatively easy to 
implement (I hope) and they shouldn't introduce any run-time overhead. 
They would only generate a compiler warning or suppressable error. (i.e 
No runtime exception) So such a construct as you have above wouldn't be 
disallowed. It'd only be that in a mode of stricter checking, the 
programmer would need to suppress the warning or error and indicate that 
the usage is OK.

Re: Safety of unprotected concurrent operations on constant objects

[Dmitry A. Kazakov]

On Mon, 12 May 2014 22:50:03 -0600, Brad Moore wrote:

> I lumped task safe programs with while loops into the 
> Potentially_Blocking category, because while loops can be used to 
> implement busy spin-loops, which can be considered a form of blocking.

Loops are used in many (if not most) lock-free algorithms. They have
bounded time, because the loop condition is that the task has been
preempted during execution of the loop body, which may happen only once,
provided scheduling is any reasonable.

>> What I had in mind are designs like:
>>
>> type T is record
>>     M : aliased Mutex;
>>     ...
>> end record;
>>
>> A safe operation on this type looks like:
>>
>>     procedure Safe_Search (X : in out T; ...) is
>>         Lock : Holder (T.M'Access);
>>     begin
>>         Unsafe_Search (X, ...);
>>     end Safe_Search;
>>
>> Here safe operations call to unsafe ones all the time and never do each
>> other because M is not reeentrant.
> 
> Thanks for the example. A good case to consider. By the rules I'm 
> thinking of, this would not be a task-safe construct however, which I 
> think is rightly so.
> 
> The Task_Safe attribute is about subprograms that can be proven to be 
> safe. This construct is unsafe, because it doesn't guarantee that there 
> aren't direct concurrent calls to Unsafe_Search happening while inside 
> the body of Safe_Search. (It would probably be too difficult to prove, 
> and so its better to assume the worst, when it comes to safety.) 
> Therefore Safe_Search is also not a task-safe call.

This is why I consider these attributes useless as they would work for
marginal cases only.

[...]

The rules you are proposing seem to me focusing on rather atomicity than
task safety.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

Re: Safety of unprotected concurrent operations on constant objects

[Brad Moore]

On 14-05-13 02:56 AM, Dmitry A. Kazakov wrote:
> On Mon, 12 May 2014 22:50:03 -0600, Brad Moore wrote:
>
>> I lumped task safe programs with while loops into the
>> Potentially_Blocking category, because while loops can be used to
>> implement busy spin-loops, which can be considered a form of blocking.
>
> Loops are used in many (if not most) lock-free algorithms. They have
> bounded time, because the loop condition is that the task has been
> preempted during execution of the loop body, which may happen only once,
> provided scheduling is any reasonable.
>
>>> What I had in mind are designs like:
>>>
>>> type T is record
>>>      M : aliased Mutex;
>>>      ...
>>> end record;
>>>
>>> A safe operation on this type looks like:
>>>
>>>      procedure Safe_Search (X : in out T; ...) is
>>>          Lock : Holder (T.M'Access);
>>>      begin
>>>          Unsafe_Search (X, ...);
>>>      end Safe_Search;
>>>
>>> Here safe operations call to unsafe ones all the time and never do each
>>> other because M is not reeentrant.
>>
>> Thanks for the example. A good case to consider. By the rules I'm
>> thinking of, this would not be a task-safe construct however, which I
>> think is rightly so.
>>
>> The Task_Safe attribute is about subprograms that can be proven to be
>> safe. This construct is unsafe, because it doesn't guarantee that there
>> aren't direct concurrent calls to Unsafe_Search happening while inside
>> the body of Safe_Search. (It would probably be too difficult to prove,
>> and so its better to assume the worst, when it comes to safety.)
>> Therefore Safe_Search is also not a task-safe call.
>
> This is why I consider these attributes useless as they would work for
> marginal cases only.

I think most of the code out there that was written for concurrency 
would probably satisfy the rules. (i.e. It doesn't seem marginal to me) 
In the case of your example, it likely could be made to satisfy the 
rules with some simple adjustments.

For example, you could fold the body of Unsafe_Search into the body of 
Safe_Search. Then you would be guaranteeing that there would be no way 
to circumvent the lock, as there is only the one entry point to your 
function. Your mutex lock function could then have the Task_Safe aspect.

Another approach would be to put the body of Unsafe_Search inside a 
protected object, again guaranteeing that there is no way to circumvent 
the protection.

I think most protected objects typically do not call unsafe subprograms.

>
> [...]
>
> The rules you are proposing seem to me focusing on rather atomicity than
> task safety.
>

The goal is to be able to say that a subprogram can be called safely, 
without erroneousness with other concurrent calls.

Atomicity plays a part of it, but subprograms such as pure functions 
that don't modify state also fall under the umbrella.

Re: Safety of unprotected concurrent operations on constant objects

[Brad Moore]

On 14-05-13 09:01 AM, Brad Moore wrote:
> For example, you could fold the body of Unsafe_Search into the body of
> Safe_Search. Then you would be guaranteeing that there would be no way
> to circumvent the lock, as there is only the one entry point to your
> function. Your mutex lock function could then have the Task_Safe aspect.

On second thought this probably wouldn't work, or I can't think of an 
example of where it could work, since the Unsafe_Search likely modifies 
some global state.

So you'd probably have to wrap the data and function in a protected 
object, which would then be Task_Safe. That may be why Ada has PO's in 
the standard, but does not provide any mutex libraries like the one you 
suggest; They are too error prone. I'd be surprised if mutexes and scope 
locks like the one in your example wouldn't have been considered for 
inclusion in the standard at some point during the history of Ada.
Ada does provide the building blocks that programmers can create such 
abstractions however, which programmers are then free to use as they wish.

Re: Safety of unprotected concurrent operations on constant objects

[Simon Wright]

Brad Moore <brad.moore@shaw.ca> writes:

> That may be why Ada has PO's in the standard, but does not provide any
> mutex libraries like the one you suggest; They are too error
> prone. I'd be surprised if mutexes and scope locks like the one in
> your example wouldn't have been considered for inclusion in the
> standard at some point during the history of Ada.  Ada does provide
> the building blocks that programmers can create such abstractions
> however, which programmers are then free to use as they wish.

I've several times seen Randy recommend use of the Containers as a way
of avoiding problems with memory allocation/deallocation, and I'd have
thought simple mutexes/locks would be just as much candidates to support
the general user.

Are they error-prone? If Joe Programmer reinvents locking, what's the
chance that there's something wrong with it?

Re: Safety of unprotected concurrent operations on constant objects

[Dmitry A. Kazakov]

On Tue, 13 May 2014 17:46:58 +0100, Simon Wright wrote:

> Brad Moore <brad.moore@shaw.ca> writes:
> 
>> That may be why Ada has PO's in the standard, but does not provide any
>> mutex libraries like the one you suggest; They are too error
>> prone. I'd be surprised if mutexes and scope locks like the one in
>> your example wouldn't have been considered for inclusion in the
>> standard at some point during the history of Ada.  Ada does provide
>> the building blocks that programmers can create such abstractions
>> however, which programmers are then free to use as they wish.
> 
> I've several times seen Randy recommend use of the Containers as a way
> of avoiding problems with memory allocation/deallocation, and I'd have
> thought simple mutexes/locks would be just as much candidates to support
> the general user.
> 
> Are they error-prone? If Joe Programmer reinvents locking, what's the
> chance that there's something wrong with it?

Usually to mutex' seize and release there are other procedures and entries
added, e.g. when mutex is used with a container like a queue. So it is not
much advantage having them in the standard library. Then there are mutex
variations like reentrant mutexes, read-write mutexes, arrays of mutexes,
ordered mutexes (in order to prevent deadlock), global (system-wide) named
mutexes etc. This is why I am sceptical that mutexes must be in the
standard library.

Much more useful IMO would be atomic operations like atomic increment,
compare and swap, and a requirement to support pragma Atomic for every
scalar type.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

Re: Safety of unprotected concurrent operations on constant objects

[Dmitry A. Kazakov]

On Tue, 13 May 2014 09:01:44 -0600, Brad Moore wrote:

> On 14-05-13 02:56 AM, Dmitry A. Kazakov wrote:
>> On Mon, 12 May 2014 22:50:03 -0600, Brad Moore wrote:
>>
>>> I lumped task safe programs with while loops into the
>>> Potentially_Blocking category, because while loops can be used to
>>> implement busy spin-loops, which can be considered a form of blocking.
>>
>> Loops are used in many (if not most) lock-free algorithms. They have
>> bounded time, because the loop condition is that the task has been
>> preempted during execution of the loop body, which may happen only once,
>> provided scheduling is any reasonable.
>>
>>>> What I had in mind are designs like:
>>>>
>>>> type T is record
>>>>      M : aliased Mutex;
>>>>      ...
>>>> end record;
>>>>
>>>> A safe operation on this type looks like:
>>>>
>>>>      procedure Safe_Search (X : in out T; ...) is
>>>>          Lock : Holder (T.M'Access);
>>>>      begin
>>>>          Unsafe_Search (X, ...);
>>>>      end Safe_Search;
>>>>
>>>> Here safe operations call to unsafe ones all the time and never do each
>>>> other because M is not reeentrant.
>>>
>>> Thanks for the example. A good case to consider. By the rules I'm
>>> thinking of, this would not be a task-safe construct however, which I
>>> think is rightly so.
>>>
>>> The Task_Safe attribute is about subprograms that can be proven to be
>>> safe. This construct is unsafe, because it doesn't guarantee that there
>>> aren't direct concurrent calls to Unsafe_Search happening while inside
>>> the body of Safe_Search. (It would probably be too difficult to prove,
>>> and so its better to assume the worst, when it comes to safety.)
>>> Therefore Safe_Search is also not a task-safe call.
>>
>> This is why I consider these attributes useless as they would work for
>> marginal cases only.
> 
> I think most of the code out there that was written for concurrency 
> would probably satisfy the rules. (i.e. It doesn't seem marginal to me) 
> In the case of your example, it likely could be made to satisfy the 
> rules with some simple adjustments.
> 
> For example, you could fold the body of Unsafe_Search into the body of 
> Safe_Search. Then you would be guaranteeing that there would be no way 
> to circumvent the lock, as there is only the one entry point to your 
> function. Your mutex lock function could then have the Task_Safe aspect.
> 
> Another approach would be to put the body of Unsafe_Search inside a 
> protected object, again guaranteeing that there is no way to circumvent 
> the protection.

No, that does not look the way it is usually used. Typically the unsafe
operation is really unsafe, e.g. it does I/O, communicates with a DB and
blocks as much as can it be. It is certainly not for a protected action and
certainly cannot be looked inside or is too complex for analysis.

> I think most protected objects typically do not call unsafe subprograms.

They do. It is an unrelated case, as I said, task safety needs to support
blocking, but still it is a usable pattern, that is to pass an unsafe
operation to a protected object's entry in order to execute it on the
context of a protected action.

I am using it this pattern in order to circumvent Ada's deficiency that
protected objects cannot be inherited from. This looks the only way to
implement an extendable a safe object. It is by delegating public
operations to protected actions of some private protected object. Extension
is achieved by passing an access to procedure to an entry point of this
private object. Of course you could prove nothing useful about this pattern
with your rules, in most case.

In any case, before messing up with attributes we should IMO concentrate
efforts on integrating SPARK into Ada and having language mandated provers
and language infrastructure supporting provers on programmer's demand, like
proper pre-/postconditions, axioms etc. Once this is in place and working
we could start thinking how to formalize concurrency aspects within this
framework. Otherwise it is putting the cart before the horse.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

Re: Safety of unprotected concurrent operations on constant objects

[Randy Brukardt]

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
news:1tb8my720vum2$.r9u7r03btzqm.dlg@40tude.net...
...
>> I think most protected objects typically do not call unsafe subprograms.
>
> They do. It is an unrelated case, as I said, task safety needs to support
> blocking, but still it is a usable pattern, that is to pass an unsafe
> operation to a protected object's entry in order to execute it on the
> context of a protected action.

I don't think you guys are even talking about the same problem. Brad's 
Task_Sfae idea (which is similar to an idea I had years ago is aimed at 
providing idiot-proof concurrency. This is necessarily going to be a rather 
small subset of all of the possibilities of concurrency. Ada surely does not 
need new ways to do complex concurrency; it has lots of ways to shoot 
yourself in the foot now, and all of the flexibility one could possibly 
want.

But for a lot of problems, bog-simple parallel execution of code is enough, 
and for that, one wants to allow a very restricted set of operations which 
prevent trouble by construction. That's the purpose of Task_Safe and similar 
ideas.

In the long run, the Ada has to have an easier way to construct parallel 
programs. Raw tasks are pretty much like programming in C, given the lack of 
any protection from making mistakes -- it's not at all like Ada in other 
areas. Whether one can do everything that they might want safely is not 
relevant.

Something like Task_Safe can be very restrictive, simply because one can 
always write separate tasks if they need something more complex. It 
certainly don't have to allow everything.

> In any case, before messing up with attributes we should IMO concentrate
> efforts on integrating SPARK into Ada and having language mandated provers
> and language infrastructure supporting provers on programmer's demand, 
> like
> proper pre-/postconditions, axioms etc. Once this is in place and working
> we could start thinking how to formalize concurrency aspects within this
> framework. Otherwise it is putting the cart before the horse.

I'm hestitant to say "never", but I think it is highly unlikely that Ada 
(the programming language) will ever include any proof technology. That's 
because it's simply too difficult to formally describe the rules involved. 
Even relatively simple rules (such as errors for always out of range values) 
are too hard to add to Ada without pages of rules or far too many false 
positives (or usually both).

If one doesn't formally describe the rules (what must and most not be 
detected), then all Ada portability is lost. In such a case, no language 
standard is needed at all (it's only real purpose is to provide an avenue 
for portability between implemetations).

With Ada 2012, we provided a framework for contracts. We have to enforce 
those at runtime in the language definition because no other solution is 
practically possible. But one hopes that implementations take those further 
and provide mechanisms to use those contracts in proof settings.

Certainly, future versions of Ada can add things that will provide 
additional help (exception contracts are near the top of the list, IMHO), 
but I don't think that we can do much to mandate proof. (Besides, I think 
that mandating proof would have the effect of driving all Ada vendors other 
than AdaCore out of the Ada business -- I very much doubt that any of the 
other compiler vendors could afford the investment. Perhaps that will happen 
anyway, given the slow uptake of Ada 2012 by other vendors.)

                                              Randy.

Re: Safety of unprotected concurrent operations on constant objects

[Shark8]

On 13-May-14 14:27, Randy Brukardt wrote:
> Perhaps that will happen
> anyway, given the slow uptake of Ada 2012 by other vendors.

Who else besides AdaCore is doing an Ada 2012 implementation?

Re: Safety of unprotected concurrent operations on constant objects

[Randy Brukardt]

"Shark8" <OneWingedShark@gmail.com> wrote in message 
news:tjCcv.246163$d32.82688@fx31.iad...
> On 13-May-14 14:27, Randy Brukardt wrote:
>> Perhaps that will happen
>> anyway, given the slow uptake of Ada 2012 by other vendors.
>
> Who else besides AdaCore is doing an Ada 2012 implementation?

Sadly, don't know of any. I've added a tiny amount of Ada 2012 stuff to 
Janus/Ada, but it will be a long time before much significant gets there.

                               Randy.

Re: Safety of unprotected concurrent operations on constant objects

[Robert A Duff]

"Randy Brukardt" <randy@rrsoftware.com> writes:

> "Shark8" <OneWingedShark@gmail.com> wrote in message 
> news:tjCcv.246163$d32.82688@fx31.iad...
>> On 13-May-14 14:27, Randy Brukardt wrote:
>>> Perhaps that will happen
>>> anyway, given the slow uptake of Ada 2012 by other vendors.
>>
>> Who else besides AdaCore is doing an Ada 2012 implementation?
>
> Sadly, don't know of any. I've added a tiny amount of Ada 2012 stuff to 
> Janus/Ada, but it will be a long time before much significant gets there.

I'd bet Atego and ICSC are working on it.

- Bob

Re: Safety of unprotected concurrent operations on constant objects

[Shark8]

On 14-May-14 15:56, Robert A Duff wrote:
> I'd bet Atego and ICSC are working on it.

Hm, what makes you think that?
The last I'd heard about Atego was their acquisition of Rational from IBM.

Re: Safety of unprotected concurrent operations on constant objects

[Brad Moore]

On 14-05-13 02:27 PM, Randy Brukardt wrote:
> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message
> news:1tb8my720vum2$.r9u7r03btzqm.dlg@40tude.net...
> ...
>>> I think most protected objects typically do not call unsafe subprograms.
>>
>> They do. It is an unrelated case, as I said, task safety needs to support
>> blocking, but still it is a usable pattern, that is to pass an unsafe
>> operation to a protected object's entry in order to execute it on the
>> context of a protected action.
>
> I don't think you guys are even talking about the same problem. Brad's
> Task_Sfae idea (which is similar to an idea I had years ago is aimed at
> providing idiot-proof concurrency. This is necessarily going to be a rather
> small subset of all of the possibilities of concurrency. Ada surely does not
> need new ways to do complex concurrency; it has lots of ways to shoot
> yourself in the foot now, and all of the flexibility one could possibly
> want.

Agreed. The Aspects I had in mind are not about coming up with new ways 
of doing concurrency, only about presenting a better picture to the 
client of the subroutine (both the compiler and the programmer), so that 
programmers can make use of concurrency or parallelism hopefully with 
less chance of shooting themselves in the foot. (i.e more safely)

>
> But for a lot of problems, bog-simple parallel execution of code is enough,
> and for that, one wants to allow a very restricted set of operations which
> prevent trouble by construction. That's the purpose of Task_Safe and similar
> ideas.

Right.

>
> In the long run, the Ada has to have an easier way to construct parallel
> programs. Raw tasks are pretty much like programming in C, given the lack of
> any protection from making mistakes -- it's not at all like Ada in other
> areas. Whether one can do everything that they might want safely is not
> relevant.
>
> Something like Task_Safe can be very restrictive, simply because one can
> always write separate tasks if they need something more complex. It
> certainly don't have to allow everything.

And also the use of Task_Safe is optional. If one wants to work in a 
less restrictive environment, they dont have to use the aspect.

>
>> In any case, before messing up with attributes we should IMO concentrate
>> efforts on integrating SPARK into Ada and having language mandated provers
>> and language infrastructure supporting provers on programmer's demand,
>> like
>> proper pre-/postconditions, axioms etc. Once this is in place and working
>> we could start thinking how to formalize concurrency aspects within this
>> framework. Otherwise it is putting the cart before the horse.
>
> I'm hestitant to say "never", but I think it is highly unlikely that Ada
> (the programming language) will ever include any proof technology. That's
> because it's simply too difficult to formally describe the rules involved.
> Even relatively simple rules (such as errors for always out of range values)
> are too hard to add to Ada without pages of rules or far too many false
> positives (or usually both).

And to be clear, when I mention proving task safety with these aspects, 
I do not mean formal proof or mathematical proof. I only mean in an 
informal manner that allows us to reason, similar to how applying pragma 
Pure to a package spec allows us to reason that the subprograms in such 
a package are safe for remote subprogram usage with the distributed 
annex. The public (visible) view of Pure on a package means the compiler 
of a client unit does not need to look into the implementation of the 
Pure package, since it knows the rules of pragma Pure have been applied 
to that package.

Brad
>
> If one doesn't formally describe the rules (what must and most not be
> detected), then all Ada portability is lost. In such a case, no language
> standard is needed at all (it's only real purpose is to provide an avenue
> for portability between implemetations).
>
> With Ada 2012, we provided a framework for contracts. We have to enforce
> those at runtime in the language definition because no other solution is
> practically possible. But one hopes that implementations take those further
> and provide mechanisms to use those contracts in proof settings.
>
> Certainly, future versions of Ada can add things that will provide
> additional help (exception contracts are near the top of the list, IMHO),
> but I don't think that we can do much to mandate proof. (Besides, I think
> that mandating proof would have the effect of driving all Ada vendors other
> than AdaCore out of the Ada business -- I very much doubt that any of the
> other compiler vendors could afford the investment. Perhaps that will happen
> anyway, given the slow uptake of Ada 2012 by other vendors.)
>
>                                                Randy.
>
>

Re: Safety of unprotected concurrent operations on constant objects

[Dmitry A. Kazakov]

On Tue, 13 May 2014 15:27:02 -0500, Randy Brukardt wrote:

> (Besides, I think 
> that mandating proof would have the effect of driving all Ada vendors other 
> than AdaCore out of the Ada business -- I very much doubt that any of the 
> other compiler vendors could afford the investment. Perhaps that will happen 
> anyway, given the slow uptake of Ada 2012 by other vendors.)

No, that is not the idea. Ada would not mandate any proofs. The programmer
will.

Task safety or whatever, will be a library of axioms and inference rules.
The language should provide means of encapsulation and reuse for
annotations.

If you don't want to annotate the contracts of your package with these, you
don't. With *proper* contracts that must have no effect on the program
semantics. Regarding legality, removing a contract cannot make a program
illegal (preconditions weakened, postconditions strengthened).

The only tricky thing the standard should define is the power of the prover
and its *weakness*. because in order to be portable the prover must reject
provable cases which other provers might not be able to prove.

You *cannot* increase the power of prover later on, as you and others seem
to suggest.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

Re: Safety of unprotected concurrent operations on constant objects

[Robert A Duff]

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> writes:

> You *cannot* increase the power of prover later on, as you and others seem
> to suggest.

Why not?

- Bob

Re: Safety of unprotected concurrent operations on constant objects

[Dmitry A. Kazakov]

On Thu, 15 May 2014 09:21:14 -0400, Robert A Duff wrote:

> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> writes:
> 
>> You *cannot* increase the power of prover later on, as you and others seem
>> to suggest.
> 
> Why not?

Because inability to prove that contract X is fulfilled by a party P makes
P illegal. [*]

Unless you accept making illegal programs legal, you must not allow the
prover's power to change.

Example from existing Ada:

   function Foo return Integer is
   begin
      raise Constraint_Error;
   end Foo;

This program is illegal, though GNAT posses the power to prove Foo's
"contract" fulfilled (vaguely: no junk result returned). Yet the language
requires this power constrained. The mandated power is that it is
non-provable that the code following raise were unreachable.

--------------
* If we talk about contracts proper. Per definition, a contract violation
makes the program illegal

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

Re: Safety of unprotected concurrent operations on constant objects

[Robert A Duff]

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> writes:

> Because inability to prove that contract X is fulfilled by a party P makes
> P illegal. [*]

I know that's your point of view.  I haven't seen you explain why.

Yeah, I know compile-time checks are good when possible.
But they're not always possible (as I'm sure you know).
So insisting on contracts being checked at compile time
doesn't make my programs better -- it just requires me to
put "--" before some of my contracts.

> Unless you accept making illegal programs legal, you must not allow the
> prover's power to change.

Every new version of Ada has made some previously-illegal programs
legal.  An infinite number of them, in fact.  So of course I 
accept making illegal programs legal.

- Bob

Re: Safety of unprotected concurrent operations on constant objects

[Dmitry A. Kazakov]

On Thu, 15 May 2014 11:53:09 -0400, Robert A Duff wrote:

> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> writes:
> 
>> Because inability to prove that contract X is fulfilled by a party P makes
>> P illegal. [*]
> 
> I know that's your point of view.  I haven't seen you explain why.

Sorry? There are three outcomes of a proof:

1. True
2. False
3. Don't know

And two outcomes of program legality:

A. Legal
B. Illegal

Now map 1,2,3 to A,B. I assume it is:

1 -> A
2 -> B
3 -> B (cannot prove it, assume it is wrong)

You?

> Yeah, I know compile-time checks are good when possible.
> But they're not always possible (as I'm sure you know).
> So insisting on contracts being checked at compile time
> doesn't make my programs better -- it just requires me to
> put "--" before some of my contracts.

?

We were talking about a prover, at least I was. I fail to see how a prover
could be related in any form to run-time. You may say that prover is not
about pseudo-contracts of Ada 2012, I don't care. Use whatever word you
want, but prover is still a compile-time.

>> Unless you accept making illegal programs legal, you must not allow the
>> prover's power to change.
> 
> Every new version of Ada has made some previously-illegal programs
> legal.  An infinite number of them, in fact.  So of course I 
> accept making illegal programs legal.

If you are OK with that, very well. Still you will have to mandate a
well-defined power within each version. Otherwise, legality will depend on
the compiler.

P.S. I thought you were against making

   function Foo return Integer is
   begin
      raise Constraint_Error;
   end Foo;

legal?

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

Re: Safety of unprotected concurrent operations on constant objects

[Jacob Sparre Andersen]

Dmitry A. Kazakov <mailbox@dmitry-kazakov.de> wrote:

> Sorry? There are three outcomes of a proof:
>
> 1. True
> 2. False
> 3. Don't know
>
> And two outcomes of program legality:
>
> A. Legal
> B. Illegal

Some of us see program legality slightly differently:

A. Known legal
B. Known illegal
C. Check at run-time

> Now map 1,2,3 to A,B. I assume it is:
>
> 1 -> A
> 2 -> B
> 3 -> B (cannot prove it, assume it is wrong)
>
> You?

Looking slightly differently at program legality it works out fine:

1 -> A
2 -> B
3 -> C

:-)

Greetings,

Jacob
-- 
"Be who you are and say what you feel, because those who mind
 don't matter and those who matter don't mind." -- Dr. Seuss

Re: Safety of unprotected concurrent operations on constant objects

[Randy Brukardt]

"Brad Moore" <brad.moore@shaw.ca> wrote in message 
news:xtDav.68151$7X2.15124@fx19.iad...
...
>> The rules you propose actually are good only for lock-free concurrency.
>
> There's million's of simple functions and procedures that do not involve 
> any locking. Integer "+" for example, is completely task safe.

I had proposed labeling such functions "super_pure" and making compile-time 
checks to ensure that is respected. That was in relation to other things 
(optimization of contract assertions), but it also applies to real-time. 
This categorization is really separate from task-safe, since it is much 
stronger than that (a super_pure function always will give the same answer 
for identical values of arguments, so one can have a version of 10.2.1(18/3) 
that applies to such functions; in additional, I'd advocate completely 
eliminating the effect of 1.1.4(18) for super_pure calls, such that parallel 
execution of them is always allowed.

[Aside: We need such permissions, even if super_pure is statically checked, 
because of the possibility of interfacing or chapter 13-ish items lying 
about the super_pure-ness of a function. We don't want compilers considering 
such lying at all; they should be able to assume that super_pure means 
task-safe.]

This idea didn't receive much traction (we ended up going with expression 
functions as a way of dealing with the contract issues), but the need really 
hasn't left. The "problem" is that a lot of things cannot be super_pure (a 
dereference, for instance, since it's effectively a reference to a global 
storage pool), so what you can do with super_pure functions is rather 
limited.

Brad is looking at ways to provide another level of task safety for more 
arbitrary stuff. That can't be checked (at least with any level of 
completeness), but a declaration of intent would be a useful thing even if 
not completely checked.

                      Randy.

Re: Safety of unprotected concurrent operations on constant objects

[Robert A Duff]

Brad Moore <brad.moore@shaw.ca> writes:

> However, it might make sense to specify certain primitive subprograms of
> a type as being task safe.

What exactly do you mean by "task safe", either for a type, or for
a subprogram?  E.g. if Element is task safe, does that mean calls
to Element are atomic with respect to each other?  If both Element
and Replace_Element are task safe, does that mean calls to Element
and Replace_Element are atomic; i.e. if one task calls Element,
and another calls Replace_Element, those two calls are serialized?

Why primitive subprograms?  What about class-wide subprograms
declared in the same package?

Does task safety imply absence of deadlock?

Suppose we have an atomic increment function (calls to it are
serialized), and Counter is initially 0, and one task does
"X := Incr (Counter);" and another task does "Y := Incr (Counter);".
A third task waits for those two to terminate, and then calls 
procedure P, which prints X followed by Y.  Is P task safe?

If the comment on P says "-- This prints 1 followed by 2.",
you've got a race condition.  But what if the comment says
"-- This prints 1 and 2, in either order." -- does that
make it task safe?

I understand task safety in an informal way, but I'm not sure
how to decribe it formally.  And if the definition depends on
the intent of the programmer (perhaps expressed in comments),
we can't expect a compiler to check it.  ;-)

- Bob

Re: Safety of unprotected concurrent operations on constant objects

[Dmitry A. Kazakov]

On Tue, 06 May 2014 12:22:59 -0400, Robert A Duff wrote:

> Brad Moore <brad.moore@shaw.ca> writes:
> 
>> However, it might make sense to specify certain primitive subprograms of
>> a type as being task safe.
> 
> What exactly do you mean by "task safe", either for a type, or for
> a subprogram?  E.g. if Element is task safe, does that mean calls
> to Element are atomic with respect to each other?

It means, in my interpretation, that the post-condition of the operation
[and the object's invariant] is true for any number of tasks Wi calling the
operation independently at any point Ti of real-time.

> If both Element
> and Replace_Element are task safe, does that mean calls to Element
> and Replace_Element are atomic; i.e. if one task calls Element,
> and another calls Replace_Element, those two calls are serialized?

No. It could be atomic in order to ensure the post-condition.

> Why primitive subprograms?  What about class-wide subprograms
> declared in the same package?

That was my question too. Presumably, primitive operations were considered
building blocks for class-wide operations, which, under this assumption,
would be safe per design for some, rather, weak [as you pointed below]
post-conditions.

> Does task safety imply absence of deadlock?

Pragmatically, the answer could be no, if more than one object involved.
Yes, for single object.

Safety of any subset of a set of objects is stronger than safety of
individual objects.

> Suppose we have an atomic increment function (calls to it are
> serialized), and Counter is initially 0, and one task does
> "X := Incr (Counter);" and another task does "Y := Incr (Counter);".
> A third task waits for those two to terminate, and then calls 
> procedure P, which prints X followed by Y.  Is P task safe?

See above, that depends on the post-condition of P.

> I understand task safety in an informal way, but I'm not sure
> how to decribe it formally.  And if the definition depends on
> the intent of the programmer (perhaps expressed in comments),
> we can't expect a compiler to check it.  ;-)

Right. Minimally, the semantics must be stated formally using pre- and
post-conditions.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

Re: Safety of unprotected concurrent operations on constant objects

[Brad Moore]

On 06/05/2014 1:07 PM, Dmitry A. Kazakov wrote:
> On Tue, 06 May 2014 12:22:59 -0400, Robert A Duff wrote:
>
>> Brad Moore <brad.moore@shaw.ca> writes:
>>
>>> However, it might make sense to specify certain primitive subprograms of
>>> a type as being task safe.
>>
>> What exactly do you mean by "task safe", either for a type, or for
>> a subprogram?  E.g. if Element is task safe, does that mean calls
>> to Element are atomic with respect to each other?
>
> It means, in my interpretation, that the post-condition of the operation
> [and the object's invariant] is true for any number of tasks Wi calling the
> operation independently at any point Ti of real-time.

That's a nice definition. It does cover a broad set of cases including 
pure functions, protected operations, sets of function calls whose 
parameters do not conflict, mutex guarded calls, etc.


>
>> If both Element
>> and Replace_Element are task safe, does that mean calls to Element
>> and Replace_Element are atomic; i.e. if one task calls Element,
>> and another calls Replace_Element, those two calls are serialized?
>
> No. It could be atomic in order to ensure the post-condition.
>
>> Why primitive subprograms?  What about class-wide subprograms
>> declared in the same package?

As explained in another email, I was worried about non-tagged types.
eg.
    type T is record ... end record with Task_Safe => True;
    type U is record ... end record with Task_Safe => False;

    function Bar (X1 : T; X2 : U) return Integer;

    It might be confusing or onerous for the reader to determine if Bar
    is task safe or not, particularly if there is a long list of
    parameters.

I think Class-wide subprograms declared in the same package however 
could probably be lumped in with the primitive functions, and the aspect 
could apply to those as well..


>
> That was my question too. Presumably, primitive operations were considered
> building blocks for class-wide operations, which, under this assumption,
> would be safe per design for some, rather, weak [as you pointed below]
> post-conditions.
>
>> Does task safety imply absence of deadlock?
>
> Pragmatically, the answer could be no, if more than one object involved.
> Yes, for single object.
>
> Safety of any subset of a set of objects is stronger than safety of
> individual objects.
>

It would be nice if it could imply the absence of deadlock, but I think 
that might be too lofty a goal.

>> Suppose we have an atomic increment function (calls to it are
>> serialized), and Counter is initially 0, and one task does
>> "X := Incr (Counter);" and another task does "Y := Incr (Counter);".
>> A third task waits for those two to terminate, and then calls
>> procedure P, which prints X followed by Y.  Is P task safe?
>
> See above, that depends on the post-condition of P.

I think non-determinism is a different property that is independent of 
task safety. There is no reason to believe P is incorrect. It may very 
well satisfy it's post-condition. as Dmitry says.

>
>> I understand task safety in an informal way, but I'm not sure
>> how to decribe it formally.  And if the definition depends on
>> the intent of the programmer (perhaps expressed in comments),
>> we can't expect a compiler to check it.  ;-)
>
> Right. Minimally, the semantics must be stated formally using pre- and
> post-conditions.
>

Even without a formal definition of task safety, the compiler could 
check that a task safe subprogram only calls other task safe 
subprograms.  (Subprograms that have been explicitly marked by the 
subprogrammer as being task safe). That'd be a good start actually.

But I think it would be better if the compiler could provide more safety.

A task safe call should probably not be a potentially blocking call, I 
think.

A task safe subprogram should also not modify global variables that 
aren't protected, or atomic.

This would add quite a bit of safety, I think but maybe there are other 
restrictions that could be added also.

Re: Safety of unprotected concurrent operations on constant objects

[Brad Moore]

On 14-05-07 11:03 PM, Brad Moore wrote:
> On 06/05/2014 1:07 PM, Dmitry A. Kazakov wrote:
>> On Tue, 06 May 2014 12:22:59 -0400, Robert A Duff wrote:
>>
>>> Brad Moore <brad.moore@shaw.ca> writes:
>>>
>>>> However, it might make sense to specify certain primitive
>>>> subprograms of
>>>> a type as being task safe.
>>>
>>> What exactly do you mean by "task safe", either for a type, or for
>>> a subprogram?  E.g. if Element is task safe, does that mean calls
>>> to Element are atomic with respect to each other?
>>
>> It means, in my interpretation, that the post-condition of the operation
>> [and the object's invariant] is true for any number of tasks Wi
>> calling the
>> operation independently at any point Ti of real-time.
>
> That's a nice definition. It does cover a broad set of cases including
> pure functions, protected operations, sets of function calls whose
> parameters do not conflict, mutex guarded calls, etc.
>
>
>>
>>> If both Element
>>> and Replace_Element are task safe, does that mean calls to Element
>>> and Replace_Element are atomic; i.e. if one task calls Element,
>>> and another calls Replace_Element, those two calls are serialized?
>>
>> No. It could be atomic in order to ensure the post-condition.
>>
>>> Why primitive subprograms?  What about class-wide subprograms
>>> declared in the same package?
>
> As explained in another email, I was worried about non-tagged types.
> eg.
>     type T is record ... end record with Task_Safe => True;
>     type U is record ... end record with Task_Safe => False;
>
>     function Bar (X1 : T; X2 : U) return Integer;
>
>     It might be confusing or onerous for the reader to determine if Bar
>     is task safe or not, particularly if there is a long list of
>     parameters.
>
> I think Class-wide subprograms declared in the same package however
> could probably be lumped in with the primitive functions, and the aspect
> could apply to those as well..
>
>
>>
>> That was my question too. Presumably, primitive operations were
>> considered
>> building blocks for class-wide operations, which, under this assumption,
>> would be safe per design for some, rather, weak [as you pointed below]
>> post-conditions.
>>
>>> Does task safety imply absence of deadlock?
>>
>> Pragmatically, the answer could be no, if more than one object involved.
>> Yes, for single object.
>>
>> Safety of any subset of a set of objects is stronger than safety of
>> individual objects.
>>
>
> It would be nice if it could imply the absence of deadlock, but I think
> that might be too lofty a goal.
>
>>> Suppose we have an atomic increment function (calls to it are
>>> serialized), and Counter is initially 0, and one task does
>>> "X := Incr (Counter);" and another task does "Y := Incr (Counter);".
>>> A third task waits for those two to terminate, and then calls
>>> procedure P, which prints X followed by Y.  Is P task safe?
>>
>> See above, that depends on the post-condition of P.
>
> I think non-determinism is a different property that is independent of
> task safety. There is no reason to believe P is incorrect. It may very
> well satisfy it's post-condition. as Dmitry says.
>
>>
>>> I understand task safety in an informal way, but I'm not sure
>>> how to decribe it formally.  And if the definition depends on
>>> the intent of the programmer (perhaps expressed in comments),
>>> we can't expect a compiler to check it.  ;-)
>>
>> Right. Minimally, the semantics must be stated formally using pre- and
>> post-conditions.
>>
>
> Even without a formal definition of task safety, the compiler could
> check that a task safe subprogram only calls other task safe
> subprograms.  (Subprograms that have been explicitly marked by the
> subprogrammer as being task safe). That'd be a good start actually.
>
> But I think it would be better if the compiler could provide more safety.
>
> A task safe call should probably not be a potentially blocking call, I
> think.
>
> A task safe subprogram should also not modify global variables that
> aren't protected, or atomic.
>
> This would add quite a bit of safety, I think but maybe there are other
> restrictions that could be added also.

Actually, I have second thoughts about disallowing calls to entries from 
a "task_safe" subprogram. It should be allowed, as the rules about 
potentially blocking operations would help prevent calling an entry from 
another entry.

But I think the idea could be carried further. Another property of a 
subprogram that is important to know is whether it is a blocking call or 
not. That is another attribute that would be nice to capture in the 
contract. I think it would be useful to have a Blocking aspect that 
could be similarly applied to a subprogram specification.

I see it working something like the following;

- A Blocking call is viewed conceptually as being a Task Safe call (as 
it should). It is a more specific kind of a task safe call.

- The Blocking aspect may be optionally applied to any subprogram, 
whether it is actually blocking or not. If the subprogram is not 
blocking, it might mean that the programmer is reserving the right to 
make it a blocking call in the future, or that other implementations of 
the specification might be blocking.

- If a subprogram directly has task or protected object entry calls, 
then it cannot be explicitly specified as having the Task_Safe aspect. 
It must instead be specified as having the Blocking aspect. 
(Alternatively the subprogram can be left without any aspect 
specification. It is only used if the programmer wants to capture these 
details in the contract of the subprogram, but then the subprogram is 
not Task Safe, i.e. the Task_Safe aspect is false)

- A Task Safe program can only call other Task_Safe subprograms or 
Blocking subprograms. If the Task_Safe subprogram calls a Blocking 
Subprogram, then it cannot be explicitly specified as having the 
Task_Safe aspect. It must instead have the Blocking Aspect specified.
(or no aspect specification, or specified as false meaning that the 
subprogram is not Task Safe, i.e. the Task_Safe aspect is false)

-- Examples
function Foo return Integer with Blocking;
function Bar return Integer with Task_Safe;

Bar cannot call Foo, unless the specification is modified to either;
    function Bar return Integer with Blocking
or
    function Bar return Integer with Task_Safe => False;
(or)
    function Bar return Integer;

Regards,
Brad

Re: Safety of unprotected concurrent operations on constant objects

[Randy Brukardt]

"Brad Moore" <brad.moore@shaw.ca> wrote in message 
news:toKav.16239$tH.8133@fx31.iad...
...
> But I think the idea could be carried further. Another property of a 
> subprogram that is important to know is whether it is a blocking call or 
> not. That is another attribute that would be nice to capture in the 
> contract. I think it would be useful to have a Blocking aspect that could 
> be similarly applied to a subprogram specification.

Don't you mean "Potentially_Blocking"? Hardly anything is unconditionally 
blocking. And Ada already has such a concept, which would make a good 
starting point for such an aspect.

                           Randy.

Re: Safety of unprotected concurrent operations on constant objects

[Brad Moore]

On 14-05-08 01:57 PM, Randy Brukardt wrote:
> "Brad Moore" <brad.moore@shaw.ca> wrote in message
> news:toKav.16239$tH.8133@fx31.iad...
> ...
>> But I think the idea could be carried further. Another property of a
>> subprogram that is important to know is whether it is a blocking call or
>> not. That is another attribute that would be nice to capture in the
>> contract. I think it would be useful to have a Blocking aspect that could
>> be similarly applied to a subprogram specification.
>
> Don't you mean "Potentially_Blocking"? Hardly anything is unconditionally
> blocking. And Ada already has such a concept, which would make a good
> starting point for such an aspect.
>
>                             Randy.
>
>
Yes, I really meant Potentially_Blocking

Re: Safety of unprotected concurrent operations on constant objects

[Natasha Kerensikova]

On 2014-05-05, Brad Moore <brad.moore@shaw.ca> wrote:
>   The implementation shall ensure that each language-defined subprogram 
> is reentrant in the sense that concurrent calls on any language-defined 
> subprogram perform as specified, so long as all parameters that could be 
> passed by reference denote nonoverlapping objects.

OK, so any concurrent access of an object through standard subprograms
is unsafe.

> Another relevant RM paragraph is;
>
> RM 9.10(11-15) which starts;
>
> "Given an action of assigning to an object, and an action of reading or 
> updating a part of the same object (or of a neighboring object if the 
> two are not independently addressable), then the execution of the 
> actions is erroneous unless the actions are sequential."

And any write makes anything else unsafe on the same object.


Now the question is, what about the rest?

Does it mean any concurrent reads of the same object, without involving
any subprogram call, is safe?

At least RM 9.10 strongly implies that array indexing is task-safe.

But what about dereferencing an access value? Is it safe to concurrently
dereference the same access value from multiple tasks?

It's hard to imagine dereferencing a pointer to be unsafe, but as we all
know access are more than mere pointers, with accessibility checks and
custom storage pools and what not.

By the way, are implicit subprograms calls, like the storage pool thing
on dereference, also covered by the non-guarantee of concurrent read safety?

Re: Safety of unprotected concurrent operations on constant objects

[Randy Brukardt]

"Natasha Kerensikova" <lithiumcat@instinctive.eu> wrote in message 
news:slrnlmft61.i0l.lithiumcat@nat.rebma.instinctive.eu...
...
> But what about dereferencing an access value? Is it safe to concurrently
> dereference the same access value from multiple tasks?
>
> It's hard to imagine dereferencing a pointer to be unsafe, but as we all
> know access are more than mere pointers, with accessibility checks and
> custom storage pools and what not.

The language only allows specific things to *not* be task-safe. You can read 
9.10 and Annex A to find out what they are. (And then tell the rest of us, 
9.10 is impentrable. :-) In particular, if 9.10 doesn't include something in 
the possible erroneous execution, then it has to be task safe. (For the 
obvious reason that the language spells out what *doesn't* have to work --  
everything else has to work in all conditions.)

> By the way, are implicit subprograms calls, like the storage pool thing
> on dereference, also covered by the non-guarantee of concurrent read 
> safety?

Yes. There's nothing special about calls to Allocate or Finalize or similar 
routines.

                           Randy.

Re: Safety of unprotected concurrent operations on constant objects

[Natasha Kerensikova]

On 2014-05-08, Randy Brukardt <randy@rrsoftware.com> wrote:
> "Natasha Kerensikova" <lithiumcat@instinctive.eu> wrote in message 
> news:slrnlmft61.i0l.lithiumcat@nat.rebma.instinctive.eu...
> ...
>> But what about dereferencing an access value? Is it safe to concurrently
>> dereference the same access value from multiple tasks?
>>
>> It's hard to imagine dereferencing a pointer to be unsafe, but as we all
>> know access are more than mere pointers, with accessibility checks and
>> custom storage pools and what not.
>
> The language only allows specific things to *not* be task-safe. You can read 
> 9.10 and Annex A to find out what they are. (And then tell the rest of us, 
> 9.10 is impentrable. :-) In particular, if 9.10 doesn't include something in 
> the possible erroneous execution, then it has to be task safe. (For the 
> obvious reason that the language spells out what *doesn't* have to work --  
> everything else has to work in all conditions.)

Actually that was not all obvious to me, so I was looking something
explicit saying that whatever isn't covered by 9.10 is fine, and got
worried for not finding one.

>> By the way, are implicit subprograms calls, like the storage pool thing
>> on dereference, also covered by the non-guarantee of concurrent read 
>> safety?
>
> Yes. There's nothing special about calls to Allocate or Finalize or similar 
> routines.

When I asked this, I had in mind the Dereference abstract procedure from
GNAT's System.Checked_Pools, because then I incorrectly believed it to
be part of standard custom storage pool.

That case is still interesting, because now there *is* something special
about that call: it replaces a feature that is "intrinsic" according to
the standard. If I understand correctly the first part of your reply,
it means that the Dereference procedure must be thread-safe, despite
taking an in out storage pool object.


So to sum it up, I can put an access-to-array in a protected object,
replace it using a protected procedure, and safely use it concurrently
as a map using a binary search in a protected function.
I can then hide the protected object in the private part, wrap it in a
thread-safe reference type to avoid limited mess, and ensure the array
is sorted before handing it to the protected object.
And then everything would be fine, right? Or am I missing something?


Thanks a lot for your insights,
Natasha

Re: Safety of unprotected concurrent operations on constant objects

[Randy Brukardt]

"Natasha Kerensikova" <lithiumcat@instinctive.eu> wrote in message 
news:slrnlmmiav.i0l.lithiumcat@nat.rebma.instinctive.eu...
> On 2014-05-08, Randy Brukardt <randy@rrsoftware.com> wrote:
...
>> The language only allows specific things to *not* be task-safe. You can 
>> read
>> 9.10 and Annex A to find out what they are. (And then tell the rest of 
>> us,
>> 9.10 is impentrable. :-) In particular, if 9.10 doesn't include something 
>> in
>> the possible erroneous execution, then it has to be task safe. (For the
>> obvious reason that the language spells out what *doesn't* have to 
>> work --
>> everything else has to work in all conditions.)
>
> Actually that was not all obvious to me, so I was looking something
> explicit saying that whatever isn't covered by 9.10 is fine, and got
> worried for not finding one.

Unless the language specifically allows "erroneous execution" or "bounded 
errors", it has to work as specified. In all ways. That's spelled out in 
1.1.3. The Standard wouldn't mean much if ignoring what it says was fine. 
(But beware of 1.1.3(6), the "impossible or impractical" exception. As a 
rule, implementors lean on that only when all else fails. But it's obviously 
a squishy construct.

The basic idea of "impractical" is that implementations shouldn't spend 
excessive resources being perfect if that doesn't make sense on the 
underlying target system. An example that recently came up involves ATC on 
Windows. Windows doesn't support external interruption of threads in most 
circumstances, so ATC isn't really going to work right on Windows (there 
will be a delay on unknown length before it actually aborts). One could make 
heroic efforts to make ATC work right (avoiding Windows threads, for 
instance), but that would have costs all over the rest of tasking and I/O --  
and those features are all a lot more common than ATC.

>>> By the way, are implicit subprograms calls, like the storage pool thing
>>> on dereference, also covered by the non-guarantee of concurrent read
>>> safety?
>>
>> Yes. There's nothing special about calls to Allocate or Finalize or 
>> similar
>> routines.
>
> When I asked this, I had in mind the Dereference abstract procedure from
> GNAT's System.Checked_Pools, because then I incorrectly believed it to
> be part of standard custom storage pool.
>
> That case is still interesting, because now there *is* something special
> about that call: it replaces a feature that is "intrinsic" according to
> the standard. If I understand correctly the first part of your reply,
> it means that the Dereference procedure must be thread-safe, despite
> taking an in out storage pool object.

Typically, once you use something implementation-defined, it's the 
implementation that gets to define the rules. So if you override 
Dereference, what effect that has is solely defined by the implementation. 
The language rules are out the window.

If one truly wants portable code, one has to stay within what the Standard 
provides.

> So to sum it up, I can put an access-to-array in a protected object,
> replace it using a protected procedure, and safely use it concurrently
> as a map using a binary search in a protected function.
> I can then hide the protected object in the private part, wrap it in a
> thread-safe reference type to avoid limited mess, and ensure the array
> is sorted before handing it to the protected object.
> And then everything would be fine, right? Or am I missing something?

I think this should work; it sounds roughly like what I did in my spam 
filter. Without seeing the details, I wouldn't want to make any 
proclamations of certainty, though.

                            Randy.

Re: Safety of unprotected concurrent operations on constant objects

[Randy Brukardt]

"Simon Wright" <simon@pushface.org> wrote in message 
news:lyzjiw7h6c.fsf@pushface.org...
> Shark8 <OneWingedShark@gmail.com> writes:
>
>> On 05-May-14 15:23, Brad Moore wrote:
>>> In GNAT any read or write operations on a container that set tamper
>>> flags are ironically not task safe
>>
>> That seems very... odd.
>
> Rationale 05 8.1 [1] says (last para)
>
>   "The general rule is given in paragraph 3 of Annex A which says "The
>   implementation shall ensure that each language defined subprogram is
>   reentrant in the sense that concurrent calls on the same subprogram
>   perform as specified, so long as all parameters that could be passed
>   by reference denote nonoverlapping objects." So in other words we
>   have to protect ourselves by using the normal techniques such as
>   protected objects when container operations are invoked concurrently
>   on the same object from multiple tasks even if the operations are
>   only reading from the container."
>
> AARM12 A.18 (5.m) [2] says
>
>   "If containers with similar functionality (but different performance
>   characteristics) are provided (by the implementation or by a
>   secondary standard), we suggest that a prefix be used to identify the
>   class of the functionality: [...] "Ada.Containers.Protected_Maps"
>   (for a map which can be accessed by multiple tasks at one time);
>   [...]"
>
> Personally I'd like to see the implication (that a standard-compliant
> implementation of Containers need not be task-safe unless the Standard
> specifies that it must be) made more visible.

Of course this is true of all Ada language-defined packages -- the basic 
rule is found in Annex A (the introductory text). You have similar issues 
with Text_IO and all other I/O, and most other packages that aren't Pure. We 
decided not to expose the implicit sharing of some things (specifically the 
Environment_Variables and the Current_Directory), so those have to be 
task-safe (mainly because they already are on many target systems, and 
they're rarely performance-critical anyway).

The real problem is that very little in Ada outside of the built-in stuff is 
required to be task-safe. One of the goals of the parallel stuff is to make 
this sort of thing more explicit; but this all dates back to Ada 83. Ada 95 
made it more explicit to avoid the worst problems (there is a story about an 
Ada 83 compiler for which very basic stuff wasn't task safe). Indeed, there 
was a bug in Janus/Ada back in the day that made integer divide not 
task-safe (on early processors, divide was a software routine, and I had 
used a library-level temporary object. Bzzzzt!). But that explicitness 
didn't go very far, because no one wanted locking overhead to turn most Ada 
programs into dogs (especially those that don't use any tasks).

                                   Randy.

Re: Safety of unprotected concurrent operations on constant objects

[Brad Moore]

On 04/05/2014 3:44 PM, Shark8 wrote:
> On 05-May-14 15:23, Brad Moore wrote:
>> In GNAT any read or write operations on a container that set tamper
>> flags are ironically not task safe
>
> That seems very... odd.

Yes, it seems that the tamper checks are good for adding safety to a 
container object, when that container object is used by a single task,
however the very same tamper checks introduce concurrency problems for
container objects when accessed by multiple tasks.

The setting of tamper checks are of the form;

             B := B + 1;

Where B is a busy flag and is a Natural, without any additional 
protection. Two tasks reading B before the assignment might result
in B only getting incremented once, for instance.

Read operations on the container that might have otherwise been task 
safe, now are not as a result of the added tamper checks.

However, while it might be possible to add protection around the tamper 
flags internally, possibly via a protected object, I think that would
significantly impact performance for containers that were never intended 
for concurrent use. So I think the current GNAT implementation is good 
for the intended purpose.

Re: Safety of unprotected concurrent operations on constant objects

[Peter Chapin]

On 2014-05-04 11:18, sbelmont700@gmail.com wrote:

>> have a map capable of concurrent reads with minimal wheel reinvention?
>>
> 
> You really can't.  You can either reinvent the wheel in your own task-safe manner, or assume-the-worst about the standard map and surround it with a mutex.  Though, as was said, the split-seconds you would burn on the mutex would be negligible when compared to the network delay of supplying the results.

I don't think the concern is with the mutex operation itself, but with
the possibility of blocking while waiting for the mutex to become
available. The mutex operation itself might only take nanoseconds but
the wait might be much longer if reads are complex or frequent.

Still, it is appropriate to wonder where the application bottleneck
would actually be. Networks tend to be slow so if the server is getting
hit hard enough to make concurrent reads of an in-memory data structure
a concern, the network may have choked long before that.

Peter

Re: Safety of unprotected concurrent operations on constant objects

[Natasha Kerensikova]

On 2014-05-04, Peter Chapin <PChapin@vtc.vsc.edu> wrote:
> On 2014-05-04 11:18, sbelmont700@gmail.com wrote:
>
>>> have a map capable of concurrent reads with minimal wheel reinvention?
>>>
>> 
>> You really can't.  You can either reinvent the wheel in your own task-safe manner, or assume-the-worst about the standard map and surround it with a mutex.  Though, as was said, the split-seconds you would burn on the mutex would be negligible when compared to the network delay of supplying the results.
>
> I don't think the concern is with the mutex operation itself, but with
> the possibility of blocking while waiting for the mutex to become
> available. The mutex operation itself might only take nanoseconds but
> the wait might be much longer if reads are complex or frequent.
>
> Still, it is appropriate to wonder where the application bottleneck
> would actually be. Networks tend to be slow so if the server is getting
> hit hard enough to make concurrent reads of an in-memory data structure
> a concern, the network may have choked long before that.

Actually my concern isn't the mutex or any bottleneck.

My concern is that right now my application is NOT correct because of
its use of unprotected shared "constant" standard containers. That
situation is NOT acceptable, despite showing no issue on the current
very light load.

So I have to find a solution. And instead of rushing on my text editor
to hack around the code, I first think about potential solutions, and
what are their strengths and weaknesses, before choosing the most
engineering sound.

For example, in some cases the constant map is better replaced with an
array indexed by the result of a function generated by
GNAT.Perfect_Hash_Generators (which I discovered thanks to the research
around this particular problem) than anything mutexed.

I thought such a process wouldn't sound as weird to the audience here...

Re: Safety of unprotected concurrent operations on constant objects

[Jeffrey Carter]

On 05/04/2014 12:46 AM, Natasha Kerensikova wrote:
>
> I have some shared resources indexed by a string, described in a
> file, and considered as constant throughout the lifetime of the program
> (with the standard scheme "restart for changes to take effect").
>
> When I have whatever indexed by a string, I immediately think Maps, and
> usually go for Ordered_Maps because they are easier to understand.
>
> Since the map is semantically constant, I use the magic word constant,
> with a function to load from file at elaboration, and everything seems
> to work fine.

So, you have

M : constant Map := F;

and you're concerned about concurrent calls to

M.Element (Key)

The reserved word constant means that you can't assign to the object or pass it 
as an [in] out parameter. It certainly says nothing about what can happen to 
things designated by an access component of the object, and unbounded containers 
should be expected to have access components.

type AI is access Integer;

C : constant AI := new Integer'(1);

V : AI := new Integer'(2);

C := V; -- illegal

C.all := 42; -- No problem

As you've noted, the ARM says nothing about task safety for containers in 
general, maps in general, or ordered maps in specific, so you can't rely on this 
being task safe. And since you have the source to GNAT's ordered map package, 
you can look at it and see that this specific implementation is not task safe.

As you note, the standard allows for simultaneous calls to protected functions, 
so in general putting the map in a protected object and allowing access through 
a protected function doesn't gain you anything. Accessing it through a protected 
procedure, however, does guarantee non-concurrent access.

Since you have access to the source of GNAT, you can see that it locks a PO even 
for function calls, so with GNAT a protected function shouldn't be a problem.

I've worked on a project that used GNAT and AWS and had many tasks accessing 
hashed maps in protected objects without problem.

If you're interested in a solution that is not GNAT-specific, the skip-list 
implementation in the PragmAda Reusable Components has a Search operation that 
is task safe. It's easy enough to use a skip list as an ordered map. You'd have 
to use a[n] [Un]Bounded_String for the key, but that shouldn't be too much of a 
problem.

The PragmARCs are available from

http://pragmada.x10hosting.com/pragmarc.htm

-- 
Jeff Carter
"Brave Sir Robin ran away."
Monty Python and the Holy Grail
59

Re: Safety of unprotected concurrent operations on constant objects

[Simon Wright]

Jeffrey Carter <spam.jrcarter.not@spam.not.acm.org> writes:

> And since you have the source to GNAT's ordered map package, you can
> look at it and see that this specific implementation is not task safe.

I had a look at it following this thread, and I have to say it's quite
challenging. Could do with some architectural documentation, I think!

Re: Safety of unprotected concurrent operations on constant objects

[Jeffrey Carter]

On 05/04/2014 12:36 PM, Simon Wright wrote:
> Jeffrey Carter <spam.jrcarter.not@spam.not.acm.org> writes:
>
>> And since you have the source to GNAT's ordered map package, you can
>> look at it and see that this specific implementation is not task safe.
>
> I had a look at it following this thread, and I have to say it's quite
> challenging. Could do with some architectural documentation, I think!

I'm taking as correct the assertion here that the implementation is not task 
safe. I haven't looked at it myself.

-- 
Jeff Carter
"Brave Sir Robin ran away."
Monty Python and the Holy Grail
59

Re: Safety of unprotected concurrent operations on constant objects

[Brad Moore]

On 04/05/2014 12:55 PM, Jeffrey Carter wrote:
> If you're interested in a solution that is not GNAT-specific, the
> skip-list implementation in the PragmAda Reusable Components has a
> Search operation that is task safe. It's easy enough to use a skip list
> as an ordered map. You'd have to use a[n] [Un]Bounded_String for the
> key, but that shouldn't be too much of a problem.
>
> The PragmARCs are available from
>
> http://pragmada.x10hosting.com/pragmarc.htm
>

You might want to also have a look at the parallel red-black trees in 
the paraffinalia folders at
http://sourceforge.net/projects/paraffin

Once the tree is populated, I think querying the tree should be task 
safe, so long as no new nodes are added or deleted. It also provides 
parallel iteration through the tree, if needed. The tree was not 
otherwise intended to be task safe, but given the description of the 
OP's needs ( a constant container object ), it might be suitable.

Re: Safety of unprotected concurrent operations on constant objects

[Shark8]

On 04-May-14 01:46, Natasha Kerensikova wrote:
> I have some shared resources indexed by a string, described in a
> file, and considered as constant throughout the lifetime of the program
> (with the standard scheme "restart for changes to take effect").

What's the problem, then, with making the entire map constant?

  Some_Map : Constant Ordered_Map:= Load_From_File;

Or, I suppose, something like wrapping it in a protected object?
(Then you have its accesses blocked off.)

----------

As a matter of last resort you could use a package:

Package Data_Map is

   Function Get( Index: String ) return Data_Type;

   No_Index : Exception;

End Data_Map;

Package Body Data_Map is

   Type Item_List is Array(Positive Range <>) of Unbounded_String;

   Function Load_From_File return Item_List is
   -- ...

   Implementation : constant Item_List:= Load_From_File;

   -- Naive linear-search; could be optimized, provided Load_From_File
   -- returns its list as a sorted list... for small data-sets this
   -- should suffice.
   Function Index_Of( Item : String ) Return Positive is
   begin
     For Index in Implementation'Range loop
      if Implementation(Index) = To_Unbounded_String(Item) then
        Return Index;
      end if;
     end loop;

     Raise No_Index;
   end Index_Of;

   Function Get( Index: String ) return Data_Type is
     Item_Number : Positive renames Index_Of(Index);
   begin
     Return Result : constant Data_Type := Implementation( Item_Number );
   end Get;

End Data_Map;

Re: Safety of unprotected concurrent operations on constant objects

[sbelmont700]

On Sunday, May 4, 2014 4:25:26 PM UTC-4, Shark8 wrote:
> 
> What's the problem, then, with making the entire map constant?
> 

The problem is assuming what a subprogram might or might not do at all, let alone how it may or may not do it, and certainly not whether that method would be task safe or not.  What makes you think the Map object has any fields at all to even be constant (instead of being a null record)?  What proof do you have that the Find subprogram even bothers to access the Map argument, let alone any constant elements?  Why do you assume that GNAT doesn't just have one massive static system-wide array that it puts every element of every container into, with some complex search algorithm that makes is appear as though you have separate objects?  Perhaps the Find subprogram sends an email to a minimum-wage secretary at AdaCore that has all your objects filed on 3x5 cards in drawers, and who then looks up your data and emails it back?  All this is going on in the private part, which means you're not allowed to answer about it one way or the other.

-sb

Re: Safety of unprotected concurrent operations on constant objects

[Dmitry A. Kazakov]

On Sun, 04 May 2014 14:25:26 -0600, Shark8 wrote:

> On 04-May-14 01:46, Natasha Kerensikova wrote:
>> I have some shared resources indexed by a string, described in a
>> file, and considered as constant throughout the lifetime of the program
>> (with the standard scheme "restart for changes to take effect").
> 
> What's the problem, then, with making the entire map constant?

That is not enough. Technically speaking all operations must be reentrant.
All arguments being immutable does not make a subprogram reentrant.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de

Re: Safety of unprotected concurrent operations on constant objects

[Randy Brukardt]

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
news:1jbqe7sd9d13f.1p91l6pdkv6fz.dlg@40tude.net...
> On Sun, 04 May 2014 14:25:26 -0600, Shark8 wrote:
>
>> On 04-May-14 01:46, Natasha Kerensikova wrote:
>>> I have some shared resources indexed by a string, described in a
>>> file, and considered as constant throughout the lifetime of the program
>>> (with the standard scheme "restart for changes to take effect").
>>
>> What's the problem, then, with making the entire map constant?
>
> That is not enough. Technically speaking all operations must be reentrant.
> All arguments being immutable does not make a subprogram reentrant.

Right. And "constant" doesn't have that effect (of immutability) for private 
types anyway. It just prevents assigning to the whole object *from the 
current view*. But it's easy to get a variable view for immutably limited 
types, and not hard for controlled types. Not to mention access-to-variable 
components. And you cannot assume that there aren't any controlled 
components or access-to-variable components for a private type.

                   Randy.

Re: Safety of unprotected concurrent operations on constant objects

[Randy Brukardt]

"Natasha Kerensikova" <lithiumcat@instinctive.eu> wrote in message 
news:slrnlm6mkg.i0l.lithiumcat@nat.rebma.instinctive.eu...
...
> Is it safe to have many tasks performing operations concurrently on
> constant objects?

Ada really doesn't have any such thing as constant objects for many types. 
The majority of "constants" of composite types are actually variables during 
some part of their lifetime (and because that variable view can be saved and 
used later, they can never be assumed to be constant). That specifically 
applies to anything with a controlled part and anything with an immutably 
limited part.

As a client, since you shouldn't be looking through private types, you have 
to assume that there is a controlled component somewhere and thus you should 
never assume *anything* is constant of a private type.

Ergo the question is meaningless for the vast majority of constant composite 
objects; they exist in name only.

                           Randy.