From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00 autolearn=unavailable autolearn_force=no version=3.4.4 Path: eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!news.eternal-september.org!news.eternal-september.org!feeder.eternal-september.org!news.glorb.com!peer01.iad.highwinds-media.com!news.highwinds-media.com!feed-me.highwinds-media.com!post01.iad.highwinds-media.com!fx11.iad.POSTED!not-for-mail From: Brad Moore User-Agent: Mozilla/5.0 (Windows NT 6.1; rv:24.0) Gecko/20100101 Thunderbird/24.5.0 MIME-Version: 1.0 Newsgroups: comp.lang.ada Subject: Re: Safety of unprotected concurrent operations on constant objects References: <7403d130-8b42-43cd-a0f1-53ba34b46141@googlegroups.com> <6c2cd5d4-a44c-4c18-81a3-a0e87d25cd9e@googlegroups.com> <6ve3i79bog3t.uojmmyur7v75.dlg@40tude.net> In-Reply-To: <6ve3i79bog3t.uojmmyur7v75.dlg@40tude.net> Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit Message-ID: NNTP-Posting-Host: 68.145.219.148 X-Complaints-To: internet.abuse@sjrb.ca X-Trace: 1399525337 68.145.219.148 (Thu, 08 May 2014 05:02:17 UTC) NNTP-Posting-Date: Thu, 08 May 2014 05:02:17 UTC Date: Wed, 07 May 2014 23:03:21 -0600 X-Received-Bytes: 5590 X-Received-Body-CRC: 2168198994 Xref: news.eternal-september.org comp.lang.ada:19746 Date: 2014-05-07T23:03:21-06:00 List-Id: 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 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.