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=-0.3 required=5.0 tests=BAYES_00,
	REPLYTO_WITHOUT_TO_CC autolearn=no autolearn_force=no version=3.4.4
Path: 
 border1.nntp.dca.giganews.com!nntp.giganews.com!usenet.blueworldhosting.com!feeder01.blueworldhosting.com!feeder.erje.net!eu.feeder.erje.net!news.ecp.fr!aioe.org!.POSTED!not-for-mail
From: "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de>
Newsgroups: comp.lang.ada
Subject: Re: Safety of unprotected concurrent operations on constant objects
Date: Mon, 5 May 2014 18:36:34 +0200
Organization: cbb software GmbH
Message-ID: <t7a0jcl05g1h.11jb75b2jg1l7.dlg@40tude.net>
References: <slrnlm6mkg.i0l.lithiumcat@nat.rebma.instinctive.eu>
	<7403d130-8b42-43cd-a0f1-53ba34b46141@googlegroups.com>
	<slrnlmals8.i0l.lithiumcat@nat.rebma.instinctive.eu>
	<lya9aybkxc.fsf@pushface.org>
 <lk41jr$1vl$1@dont-email.me>
	<slrnlmbs1n.i0l.lithiumcat@nat.rebma.instinctive.eu>
	<6c2cd5d4-a44c-4c18-81a3-a0e87d25cd9e@googlegroups.com>
	<slrnlmcoqd.i0l.lithiumcat@nat.rebma.instinctive.eu>
	<waw9v.109142$f85.65293@fx19.iad>
 <scy9v.1071029$2N5.142769@fx05.iad>	<kxy9v.109149$f85.89664@fx19.iad>
 <lyzjiw7h6c.fsf@pushface.org> <fRN9v.204655$Ng5.180587@fx17.iad>
Reply-To: mailbox@dmitry-kazakov.de
NNTP-Posting-Host: AuYlnUSfTZrfhAkRjyySpQ.user.speranza.aioe.org
Mime-Version: 1.0
Content-Type: text/plain; charset="us-ascii"
Content-Transfer-Encoding: 7bit
X-Complaints-To: abuse@aioe.org
User-Agent: 40tude_Dialog/2.0.15.1
X-Notice: Filtered by postfilter v. 0.8.2
Xref: number.nntp.dca.giganews.com comp.lang.ada:186244
Date: 2014-05-05T18:36:34+02:00
List-Id: <comp.lang.ada>

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