* Safety of unprotected concurrent operations on constant objects @ 2014-05-02 8:42 Natasha Kerensikova 2014-05-03 13:43 ` sbelmont700 2014-05-08 3:19 ` Randy Brukardt 0 siblings, 2 replies; 94+ messages in thread From: Natasha Kerensikova @ 2014-05-02 8:42 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 94+ messages in thread
* Re: Safety of unprotected concurrent operations on constant objects 2014-05-02 8:42 Safety of unprotected concurrent operations on constant objects Natasha Kerensikova @ 2014-05-03 13:43 ` sbelmont700 2014-05-03 20:54 ` Natasha Kerensikova 2014-05-08 3:19 ` Randy Brukardt 1 sibling, 1 reply; 94+ messages in thread From: sbelmont700 @ 2014-05-03 13:43 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 94+ messages in thread
* Re: Safety of unprotected concurrent operations on constant objects 2014-05-03 13:43 ` sbelmont700 @ 2014-05-03 20:54 ` Natasha Kerensikova 2014-05-03 21:40 ` Simon Wright 0 siblings, 1 reply; 94+ messages in thread From: Natasha Kerensikova @ 2014-05-03 20:54 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 94+ messages in thread
* Re: Safety of unprotected concurrent operations on constant objects 2014-05-03 20:54 ` Natasha Kerensikova @ 2014-05-03 21:40 ` Simon Wright 2014-05-04 0:28 ` Jeffrey Carter 0 siblings, 1 reply; 94+ messages in thread From: Simon Wright @ 2014-05-03 21:40 UTC (permalink / raw) 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. ^ permalink raw reply [flat|nested] 94+ messages in thread
* Re: Safety of unprotected concurrent operations on constant objects 2014-05-03 21:40 ` Simon Wright @ 2014-05-04 0:28 ` Jeffrey Carter 2014-05-04 7:46 ` Natasha Kerensikova 0 siblings, 1 reply; 94+ messages in thread From: Jeffrey Carter @ 2014-05-04 0:28 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 94+ messages in thread
* Re: Safety of unprotected concurrent operations on constant objects 2014-05-04 0:28 ` Jeffrey Carter @ 2014-05-04 7:46 ` Natasha Kerensikova 2014-05-04 8:06 ` Dmitry A. Kazakov ` (3 more replies) 0 siblings, 4 replies; 94+ messages in thread From: Natasha Kerensikova @ 2014-05-04 7:46 UTC (permalink / raw) 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? ^ permalink raw reply [flat|nested] 94+ messages in thread
* Re: Safety of unprotected concurrent operations on constant objects 2014-05-04 7:46 ` Natasha Kerensikova @ 2014-05-04 8:06 ` Dmitry A. Kazakov 2014-05-04 15:18 ` sbelmont700 ` (2 subsequent siblings) 3 siblings, 0 replies; 94+ messages in thread From: Dmitry A. Kazakov @ 2014-05-04 8:06 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 94+ messages in thread
* Re: Safety of unprotected concurrent operations on constant objects 2014-05-04 7:46 ` Natasha Kerensikova 2014-05-04 8:06 ` Dmitry A. Kazakov @ 2014-05-04 15:18 ` sbelmont700 2014-05-04 15:57 ` Natasha Kerensikova 2014-05-04 16:04 ` Peter Chapin 2014-05-04 18:55 ` Jeffrey Carter 2014-05-04 20:25 ` Shark8 3 siblings, 2 replies; 94+ messages in thread From: sbelmont700 @ 2014-05-04 15:18 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 94+ messages in thread
* Re: Safety of unprotected concurrent operations on constant objects 2014-05-04 15:18 ` sbelmont700 @ 2014-05-04 15:57 ` Natasha Kerensikova 2014-05-04 18:30 ` sbelmont700 2014-05-05 19:04 ` Brad Moore 2014-05-04 16:04 ` Peter Chapin 1 sibling, 2 replies; 94+ messages in thread From: Natasha Kerensikova @ 2014-05-04 15:57 UTC (permalink / raw) 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? ^ permalink raw reply [flat|nested] 94+ messages in thread
* Re: Safety of unprotected concurrent operations on constant objects 2014-05-04 15:57 ` Natasha Kerensikova @ 2014-05-04 18:30 ` sbelmont700 2014-05-04 19:34 ` Dmitry A. Kazakov 2014-05-05 19:04 ` Brad Moore 1 sibling, 1 reply; 94+ messages in thread From: sbelmont700 @ 2014-05-04 18:30 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 94+ messages in thread
* Re: Safety of unprotected concurrent operations on constant objects 2014-05-04 18:30 ` sbelmont700 @ 2014-05-04 19:34 ` Dmitry A. Kazakov 0 siblings, 0 replies; 94+ messages in thread From: Dmitry A. Kazakov @ 2014-05-04 19:34 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 94+ messages in thread
* Re: Safety of unprotected concurrent operations on constant objects 2014-05-04 15:57 ` Natasha Kerensikova 2014-05-04 18:30 ` sbelmont700 @ 2014-05-05 19:04 ` Brad Moore 2014-05-05 21:23 ` Brad Moore 1 sibling, 1 reply; 94+ messages in thread From: Brad Moore @ 2014-05-05 19:04 UTC (permalink / raw) 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? > ^ permalink raw reply [flat|nested] 94+ messages in thread
* Re: Safety of unprotected concurrent operations on constant objects 2014-05-05 19:04 ` Brad Moore @ 2014-05-05 21:23 ` Brad Moore 2014-05-04 21:44 ` Shark8 0 siblings, 1 reply; 94+ messages in thread From: Brad Moore @ 2014-05-05 21:23 UTC (permalink / raw) 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. ^ permalink raw reply [flat|nested] 94+ messages in thread
* Re: Safety of unprotected concurrent operations on constant objects 2014-05-05 21:23 ` Brad Moore @ 2014-05-04 21:44 ` Shark8 2014-05-05 8:39 ` Simon Wright 2014-05-05 22:30 ` Brad Moore 0 siblings, 2 replies; 94+ messages in thread From: Shark8 @ 2014-05-04 21:44 UTC (permalink / raw) 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. ^ permalink raw reply [flat|nested] 94+ messages in thread
* Re: Safety of unprotected concurrent operations on constant objects 2014-05-04 21:44 ` Shark8 @ 2014-05-05 8:39 ` Simon Wright 2014-05-05 15:11 ` Brad Moore 2014-05-08 3:12 ` Randy Brukardt 2014-05-05 22:30 ` Brad Moore 1 sibling, 2 replies; 94+ messages in thread From: Simon Wright @ 2014-05-05 8:39 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 94+ messages in thread
* Re: Safety of unprotected concurrent operations on constant objects 2014-05-05 8:39 ` Simon Wright @ 2014-05-05 15:11 ` Brad Moore 2014-05-05 16:36 ` Dmitry A. Kazakov 2014-05-05 20:29 ` Natasha Kerensikova 2014-05-08 3:12 ` Randy Brukardt 1 sibling, 2 replies; 94+ messages in thread From: Brad Moore @ 2014-05-05 15:11 UTC (permalink / raw) 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. ^ permalink raw reply [flat|nested] 94+ messages in thread
* Re: Safety of unprotected concurrent operations on constant objects 2014-05-05 15:11 ` Brad Moore @ 2014-05-05 16:36 ` Dmitry A. Kazakov 2014-05-06 6:00 ` Brad Moore 2014-05-05 20:29 ` Natasha Kerensikova 1 sibling, 1 reply; 94+ messages in thread From: Dmitry A. Kazakov @ 2014-05-05 16:36 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 94+ messages in thread
* Re: Safety of unprotected concurrent operations on constant objects 2014-05-05 16:36 ` Dmitry A. Kazakov @ 2014-05-06 6:00 ` Brad Moore 2014-05-06 8:11 ` Dmitry A. Kazakov 2014-05-06 16:22 ` Robert A Duff 0 siblings, 2 replies; 94+ messages in thread From: Brad Moore @ 2014-05-06 6:00 UTC (permalink / raw) 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. ^ permalink raw reply [flat|nested] 94+ messages in thread
* Re: Safety of unprotected concurrent operations on constant objects 2014-05-06 6:00 ` Brad Moore @ 2014-05-06 8:11 ` Dmitry A. Kazakov 2014-05-06 8:48 ` Alejandro R. Mosteo ` (2 more replies) 2014-05-06 16:22 ` Robert A Duff 1 sibling, 3 replies; 94+ messages in thread From: Dmitry A. Kazakov @ 2014-05-06 8:11 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 94+ messages in thread
* Re: Safety of unprotected concurrent operations on constant objects 2014-05-06 8:11 ` Dmitry A. Kazakov @ 2014-05-06 8:48 ` Alejandro R. Mosteo 2014-05-06 9:49 ` G.B. 2014-05-07 14:04 ` Safety of unprotected concurrent operations on constant objects G.B. 2014-05-08 4:12 ` Brad Moore 2 siblings, 1 reply; 94+ messages in thread From: Alejandro R. Mosteo @ 2014-05-06 8:48 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 94+ messages in thread
* Re: Safety of unprotected concurrent operations on constant objects 2014-05-06 8:48 ` Alejandro R. Mosteo @ 2014-05-06 9:49 ` G.B. 2014-05-06 12:19 ` Dmitry A. Kazakov 0 siblings, 1 reply; 94+ messages in thread From: G.B. @ 2014-05-06 9:49 UTC (permalink / raw) 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.) ^ permalink raw reply [flat|nested] 94+ messages in thread
* Re: Safety of unprotected concurrent operations on constant objects 2014-05-06 9:49 ` G.B. @ 2014-05-06 12:19 ` Dmitry A. Kazakov 2014-05-06 12:58 ` G.B. 0 siblings, 1 reply; 94+ messages in thread From: Dmitry A. Kazakov @ 2014-05-06 12:19 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 94+ messages in thread
* Re: Safety of unprotected concurrent operations on constant objects 2014-05-06 12:19 ` Dmitry A. Kazakov @ 2014-05-06 12:58 ` G.B. 2014-05-06 15:00 ` Dmitry A. Kazakov 0 siblings, 1 reply; 94+ messages in thread From: G.B. @ 2014-05-06 12:58 UTC (permalink / raw) 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. ^ permalink raw reply [flat|nested] 94+ messages in thread
* Re: Safety of unprotected concurrent operations on constant objects 2014-05-06 12:58 ` G.B. @ 2014-05-06 15:00 ` Dmitry A. Kazakov 2014-05-06 16:24 ` G.B. 2014-05-07 4:59 ` J-P. Rosen 0 siblings, 2 replies; 94+ messages in thread From: Dmitry A. Kazakov @ 2014-05-06 15:00 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 94+ messages in thread
* Re: Safety of unprotected concurrent operations on constant objects 2014-05-06 15:00 ` Dmitry A. Kazakov @ 2014-05-06 16:24 ` G.B. 2014-05-06 19:14 ` Dmitry A. Kazakov 2014-05-07 4:59 ` J-P. Rosen 1 sibling, 1 reply; 94+ messages in thread From: G.B. @ 2014-05-06 16:24 UTC (permalink / raw) 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.) ^ permalink raw reply [flat|nested] 94+ messages in thread
* Re: Safety of unprotected concurrent operations on constant objects 2014-05-06 16:24 ` G.B. @ 2014-05-06 19:14 ` Dmitry A. Kazakov 2014-05-07 6:49 ` Georg Bauhaus 0 siblings, 1 reply; 94+ messages in thread From: Dmitry A. Kazakov @ 2014-05-06 19:14 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 94+ messages in thread
* Re: Safety of unprotected concurrent operations on constant objects 2014-05-06 19:14 ` Dmitry A. Kazakov @ 2014-05-07 6:49 ` Georg Bauhaus 2014-05-07 7:40 ` Dmitry A. Kazakov 0 siblings, 1 reply; 94+ messages in thread From: Georg Bauhaus @ 2014-05-07 6:49 UTC (permalink / raw) 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. ^ permalink raw reply [flat|nested] 94+ messages in thread
* Re: Safety of unprotected concurrent operations on constant objects 2014-05-07 6:49 ` Georg Bauhaus @ 2014-05-07 7:40 ` Dmitry A. Kazakov 2014-05-07 11:25 ` G.B. 0 siblings, 1 reply; 94+ messages in thread From: Dmitry A. Kazakov @ 2014-05-07 7:40 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 94+ messages in thread
* Re: Safety of unprotected concurrent operations on constant objects 2014-05-07 7:40 ` Dmitry A. Kazakov @ 2014-05-07 11:25 ` G.B. 2014-05-07 12:14 ` Dmitry A. Kazakov 2014-05-07 17:45 ` Simon Wright 0 siblings, 2 replies; 94+ messages in thread From: G.B. @ 2014-05-07 11:25 UTC (permalink / raw) 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. ^ permalink raw reply [flat|nested] 94+ messages in thread
* Re: Safety of unprotected concurrent operations on constant objects 2014-05-07 11:25 ` G.B. @ 2014-05-07 12:14 ` Dmitry A. Kazakov 2014-05-07 13:45 ` G.B. 2014-05-07 17:45 ` Simon Wright 1 sibling, 1 reply; 94+ messages in thread From: Dmitry A. Kazakov @ 2014-05-07 12:14 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 94+ messages in thread
* Re: Safety of unprotected concurrent operations on constant objects 2014-05-07 12:14 ` Dmitry A. Kazakov @ 2014-05-07 13:45 ` G.B. 2014-05-07 14:08 ` Dmitry A. Kazakov 0 siblings, 1 reply; 94+ messages in thread From: G.B. @ 2014-05-07 13:45 UTC (permalink / raw) 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. ^ permalink raw reply [flat|nested] 94+ messages in thread
* Re: Safety of unprotected concurrent operations on constant objects 2014-05-07 13:45 ` G.B. @ 2014-05-07 14:08 ` Dmitry A. Kazakov 0 siblings, 0 replies; 94+ messages in thread From: Dmitry A. Kazakov @ 2014-05-07 14:08 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 94+ messages in thread
* Re: Safety of unprotected concurrent operations on constant objects 2014-05-07 11:25 ` G.B. 2014-05-07 12:14 ` Dmitry A. Kazakov @ 2014-05-07 17:45 ` Simon Wright 2014-05-07 18:28 ` Georg Bauhaus 1 sibling, 1 reply; 94+ messages in thread From: Simon Wright @ 2014-05-07 17:45 UTC (permalink / raw) "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. ^ permalink raw reply [flat|nested] 94+ messages in thread
* Re: Safety of unprotected concurrent operations on constant objects 2014-05-07 17:45 ` Simon Wright @ 2014-05-07 18:28 ` Georg Bauhaus 0 siblings, 0 replies; 94+ messages in thread From: Georg Bauhaus @ 2014-05-07 18:28 UTC (permalink / raw) 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. ^ permalink raw reply [flat|nested] 94+ messages in thread
* Re: Safety of unprotected concurrent operations on constant objects 2014-05-06 15:00 ` Dmitry A. Kazakov 2014-05-06 16:24 ` G.B. @ 2014-05-07 4:59 ` J-P. Rosen 2014-05-07 7:30 ` Dmitry A. Kazakov 1 sibling, 1 reply; 94+ messages in thread From: J-P. Rosen @ 2014-05-07 4:59 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 94+ messages in thread
* Re: Safety of unprotected concurrent operations on constant objects 2014-05-07 4:59 ` J-P. Rosen @ 2014-05-07 7:30 ` Dmitry A. Kazakov 2014-05-07 8:26 ` J-P. Rosen 0 siblings, 1 reply; 94+ messages in thread From: Dmitry A. Kazakov @ 2014-05-07 7:30 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 94+ messages in thread
* Re: Safety of unprotected concurrent operations on constant objects 2014-05-07 7:30 ` Dmitry A. Kazakov @ 2014-05-07 8:26 ` J-P. Rosen 2014-05-07 9:09 ` Dmitry A. Kazakov 0 siblings, 1 reply; 94+ messages in thread From: J-P. Rosen @ 2014-05-07 8:26 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 94+ messages in thread
* Re: Safety of unprotected concurrent operations on constant objects 2014-05-07 8:26 ` J-P. Rosen @ 2014-05-07 9:09 ` Dmitry A. Kazakov 2014-05-07 11:29 ` J-P. Rosen 0 siblings, 1 reply; 94+ messages in thread From: Dmitry A. Kazakov @ 2014-05-07 9:09 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 94+ messages in thread
* Re: Safety of unprotected concurrent operations on constant objects 2014-05-07 9:09 ` Dmitry A. Kazakov @ 2014-05-07 11:29 ` J-P. Rosen 2014-05-07 12:36 ` Safety of unprotected concurrent operations on constant objects (was: Safety of unprotected concurrent operations on constant objects) Dmitry A. Kazakov 0 siblings, 1 reply; 94+ messages in thread From: J-P. Rosen @ 2014-05-07 11:29 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 94+ messages in thread
* Re: Safety of unprotected concurrent operations on constant objects (was: Safety of unprotected concurrent operations on constant objects) 2014-05-07 11:29 ` J-P. Rosen @ 2014-05-07 12:36 ` Dmitry A. Kazakov 0 siblings, 0 replies; 94+ messages in thread From: Dmitry A. Kazakov @ 2014-05-07 12:36 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 94+ messages in thread
* Re: Safety of unprotected concurrent operations on constant objects 2014-05-06 8:11 ` Dmitry A. Kazakov 2014-05-06 8:48 ` Alejandro R. Mosteo @ 2014-05-07 14:04 ` G.B. 2014-05-08 4:12 ` Brad Moore 2 siblings, 0 replies; 94+ messages in thread From: G.B. @ 2014-05-07 14:04 UTC (permalink / raw) 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. ^ permalink raw reply [flat|nested] 94+ messages in thread
* Re: Safety of unprotected concurrent operations on constant objects 2014-05-06 8:11 ` Dmitry A. Kazakov 2014-05-06 8:48 ` Alejandro R. Mosteo 2014-05-07 14:04 ` Safety of unprotected concurrent operations on constant objects G.B. @ 2014-05-08 4:12 ` Brad Moore 2014-05-08 8:20 ` Dmitry A. Kazakov 2014-05-08 19:52 ` Randy Brukardt 2 siblings, 2 replies; 94+ messages in thread From: Brad Moore @ 2014-05-08 4:12 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 94+ messages in thread
* Re: Safety of unprotected concurrent operations on constant objects 2014-05-08 4:12 ` Brad Moore @ 2014-05-08 8:20 ` Dmitry A. Kazakov 2014-05-08 10:30 ` G.B. 2014-05-09 13:14 ` Brad Moore 2014-05-08 19:52 ` Randy Brukardt 1 sibling, 2 replies; 94+ messages in thread From: Dmitry A. Kazakov @ 2014-05-08 8:20 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 94+ messages in thread
* Re: Safety of unprotected concurrent operations on constant objects 2014-05-08 8:20 ` Dmitry A. Kazakov @ 2014-05-08 10:30 ` G.B. 2014-05-09 13:14 ` Brad Moore 1 sibling, 0 replies; 94+ messages in thread From: G.B. @ 2014-05-08 10:30 UTC (permalink / raw) 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. ^ permalink raw reply [flat|nested] 94+ messages in thread
* Re: Safety of unprotected concurrent operations on constant objects 2014-05-08 8:20 ` Dmitry A. Kazakov 2014-05-08 10:30 ` G.B. @ 2014-05-09 13:14 ` Brad Moore 2014-05-09 19:00 ` Dmitry A. Kazakov 1 sibling, 1 reply; 94+ messages in thread From: Brad Moore @ 2014-05-09 13:14 UTC (permalink / raw) 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. > ^ permalink raw reply [flat|nested] 94+ messages in thread
* Re: Safety of unprotected concurrent operations on constant objects 2014-05-09 13:14 ` Brad Moore @ 2014-05-09 19:00 ` Dmitry A. Kazakov 2014-05-10 12:30 ` Brad Moore 0 siblings, 1 reply; 94+ messages in thread From: Dmitry A. Kazakov @ 2014-05-09 19:00 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 94+ messages in thread
* Re: Safety of unprotected concurrent operations on constant objects 2014-05-09 19:00 ` Dmitry A. Kazakov @ 2014-05-10 12:30 ` Brad Moore 2014-05-10 20:27 ` Dmitry A. Kazakov 0 siblings, 1 reply; 94+ messages in thread From: Brad Moore @ 2014-05-10 12:30 UTC (permalink / raw) 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. > ^ permalink raw reply [flat|nested] 94+ messages in thread
* Re: Safety of unprotected concurrent operations on constant objects 2014-05-10 12:30 ` Brad Moore @ 2014-05-10 20:27 ` Dmitry A. Kazakov 2014-05-11 6:56 ` Brad Moore 2014-05-11 18:01 ` Brad Moore 0 siblings, 2 replies; 94+ messages in thread From: Dmitry A. Kazakov @ 2014-05-10 20:27 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 94+ messages in thread
* Re: Safety of unprotected concurrent operations on constant objects 2014-05-10 20:27 ` Dmitry A. Kazakov @ 2014-05-11 6:56 ` Brad Moore 2014-05-11 18:01 ` Brad Moore 1 sibling, 0 replies; 94+ messages in thread From: Brad Moore @ 2014-05-11 6:56 UTC (permalink / raw) 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. > ^ permalink raw reply [flat|nested] 94+ messages in thread
* Re: Safety of unprotected concurrent operations on constant objects 2014-05-10 20:27 ` Dmitry A. Kazakov 2014-05-11 6:56 ` Brad Moore @ 2014-05-11 18:01 ` Brad Moore 2014-05-12 8:13 ` Dmitry A. Kazakov 1 sibling, 1 reply; 94+ messages in thread From: Brad Moore @ 2014-05-11 18:01 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 94+ messages in thread
* Re: Safety of unprotected concurrent operations on constant objects 2014-05-11 18:01 ` Brad Moore @ 2014-05-12 8:13 ` Dmitry A. Kazakov 2014-05-13 4:50 ` Brad Moore 0 siblings, 1 reply; 94+ messages in thread From: Dmitry A. Kazakov @ 2014-05-12 8:13 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 94+ messages in thread
* Re: Safety of unprotected concurrent operations on constant objects 2014-05-12 8:13 ` Dmitry A. Kazakov @ 2014-05-13 4:50 ` Brad Moore 2014-05-13 8:56 ` Dmitry A. Kazakov 0 siblings, 1 reply; 94+ messages in thread From: Brad Moore @ 2014-05-13 4:50 UTC (permalink / raw) 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. ^ permalink raw reply [flat|nested] 94+ messages in thread
* Re: Safety of unprotected concurrent operations on constant objects 2014-05-13 4:50 ` Brad Moore @ 2014-05-13 8:56 ` Dmitry A. Kazakov 2014-05-13 15:01 ` Brad Moore 0 siblings, 1 reply; 94+ messages in thread From: Dmitry A. Kazakov @ 2014-05-13 8:56 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 94+ messages in thread
* Re: Safety of unprotected concurrent operations on constant objects 2014-05-13 8:56 ` Dmitry A. Kazakov @ 2014-05-13 15:01 ` Brad Moore 2014-05-13 15:38 ` Brad Moore 2014-05-13 16:08 ` Dmitry A. Kazakov 0 siblings, 2 replies; 94+ messages in thread From: Brad Moore @ 2014-05-13 15:01 UTC (permalink / raw) 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. ^ permalink raw reply [flat|nested] 94+ messages in thread
* Re: Safety of unprotected concurrent operations on constant objects 2014-05-13 15:01 ` Brad Moore @ 2014-05-13 15:38 ` Brad Moore 2014-05-13 16:46 ` Simon Wright 2014-05-13 16:08 ` Dmitry A. Kazakov 1 sibling, 1 reply; 94+ messages in thread From: Brad Moore @ 2014-05-13 15:38 UTC (permalink / raw) 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. ^ permalink raw reply [flat|nested] 94+ messages in thread
* Re: Safety of unprotected concurrent operations on constant objects 2014-05-13 15:38 ` Brad Moore @ 2014-05-13 16:46 ` Simon Wright 2014-05-13 19:15 ` Dmitry A. Kazakov 0 siblings, 1 reply; 94+ messages in thread From: Simon Wright @ 2014-05-13 16:46 UTC (permalink / raw) 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? ^ permalink raw reply [flat|nested] 94+ messages in thread
* Re: Safety of unprotected concurrent operations on constant objects 2014-05-13 16:46 ` Simon Wright @ 2014-05-13 19:15 ` Dmitry A. Kazakov 0 siblings, 0 replies; 94+ messages in thread From: Dmitry A. Kazakov @ 2014-05-13 19:15 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 94+ messages in thread
* Re: Safety of unprotected concurrent operations on constant objects 2014-05-13 15:01 ` Brad Moore 2014-05-13 15:38 ` Brad Moore @ 2014-05-13 16:08 ` Dmitry A. Kazakov 2014-05-13 20:27 ` Randy Brukardt 1 sibling, 1 reply; 94+ messages in thread From: Dmitry A. Kazakov @ 2014-05-13 16:08 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 94+ messages in thread
* Re: Safety of unprotected concurrent operations on constant objects 2014-05-13 16:08 ` Dmitry A. Kazakov @ 2014-05-13 20:27 ` Randy Brukardt 2014-05-14 4:30 ` Shark8 ` (2 more replies) 0 siblings, 3 replies; 94+ messages in thread From: Randy Brukardt @ 2014-05-13 20:27 UTC (permalink / raw) "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. ^ permalink raw reply [flat|nested] 94+ messages in thread
* Re: Safety of unprotected concurrent operations on constant objects 2014-05-13 20:27 ` Randy Brukardt @ 2014-05-14 4:30 ` Shark8 2014-05-14 21:37 ` Randy Brukardt 2014-05-14 14:30 ` Brad Moore 2014-05-15 8:03 ` Dmitry A. Kazakov 2 siblings, 1 reply; 94+ messages in thread From: Shark8 @ 2014-05-14 4:30 UTC (permalink / raw) 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? ^ permalink raw reply [flat|nested] 94+ messages in thread
* Re: Safety of unprotected concurrent operations on constant objects 2014-05-14 4:30 ` Shark8 @ 2014-05-14 21:37 ` Randy Brukardt 2014-05-14 21:56 ` Robert A Duff 0 siblings, 1 reply; 94+ messages in thread From: Randy Brukardt @ 2014-05-14 21:37 UTC (permalink / raw) "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. ^ permalink raw reply [flat|nested] 94+ messages in thread
* Re: Safety of unprotected concurrent operations on constant objects 2014-05-14 21:37 ` Randy Brukardt @ 2014-05-14 21:56 ` Robert A Duff 2014-05-15 1:21 ` Shark8 0 siblings, 1 reply; 94+ messages in thread From: Robert A Duff @ 2014-05-14 21:56 UTC (permalink / raw) "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 ^ permalink raw reply [flat|nested] 94+ messages in thread
* Re: Safety of unprotected concurrent operations on constant objects 2014-05-14 21:56 ` Robert A Duff @ 2014-05-15 1:21 ` Shark8 0 siblings, 0 replies; 94+ messages in thread From: Shark8 @ 2014-05-15 1:21 UTC (permalink / raw) 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. ^ permalink raw reply [flat|nested] 94+ messages in thread
* Re: Safety of unprotected concurrent operations on constant objects 2014-05-13 20:27 ` Randy Brukardt 2014-05-14 4:30 ` Shark8 @ 2014-05-14 14:30 ` Brad Moore 2014-05-15 8:03 ` Dmitry A. Kazakov 2 siblings, 0 replies; 94+ messages in thread From: Brad Moore @ 2014-05-14 14:30 UTC (permalink / raw) 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. > > ^ permalink raw reply [flat|nested] 94+ messages in thread
* Re: Safety of unprotected concurrent operations on constant objects 2014-05-13 20:27 ` Randy Brukardt 2014-05-14 4:30 ` Shark8 2014-05-14 14:30 ` Brad Moore @ 2014-05-15 8:03 ` Dmitry A. Kazakov 2014-05-15 13:21 ` Robert A Duff 2 siblings, 1 reply; 94+ messages in thread From: Dmitry A. Kazakov @ 2014-05-15 8:03 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 94+ messages in thread
* Re: Safety of unprotected concurrent operations on constant objects 2014-05-15 8:03 ` Dmitry A. Kazakov @ 2014-05-15 13:21 ` Robert A Duff 2014-05-15 14:27 ` Dmitry A. Kazakov 0 siblings, 1 reply; 94+ messages in thread From: Robert A Duff @ 2014-05-15 13:21 UTC (permalink / raw) "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 ^ permalink raw reply [flat|nested] 94+ messages in thread
* Re: Safety of unprotected concurrent operations on constant objects 2014-05-15 13:21 ` Robert A Duff @ 2014-05-15 14:27 ` Dmitry A. Kazakov 2014-05-15 15:53 ` Robert A Duff 0 siblings, 1 reply; 94+ messages in thread From: Dmitry A. Kazakov @ 2014-05-15 14:27 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 94+ messages in thread
* Re: Safety of unprotected concurrent operations on constant objects 2014-05-15 14:27 ` Dmitry A. Kazakov @ 2014-05-15 15:53 ` Robert A Duff 2014-05-15 16:30 ` Dmitry A. Kazakov 0 siblings, 1 reply; 94+ messages in thread From: Robert A Duff @ 2014-05-15 15:53 UTC (permalink / raw) "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 ^ permalink raw reply [flat|nested] 94+ messages in thread
* Re: Safety of unprotected concurrent operations on constant objects 2014-05-15 15:53 ` Robert A Duff @ 2014-05-15 16:30 ` Dmitry A. Kazakov 2014-10-26 17:11 ` Jacob Sparre Andersen 0 siblings, 1 reply; 94+ messages in thread From: Dmitry A. Kazakov @ 2014-05-15 16:30 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 94+ messages in thread
* Re: Safety of unprotected concurrent operations on constant objects 2014-05-15 16:30 ` Dmitry A. Kazakov @ 2014-10-26 17:11 ` Jacob Sparre Andersen 0 siblings, 0 replies; 94+ messages in thread From: Jacob Sparre Andersen @ 2014-10-26 17:11 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 94+ messages in thread
* Re: Safety of unprotected concurrent operations on constant objects 2014-05-08 4:12 ` Brad Moore 2014-05-08 8:20 ` Dmitry A. Kazakov @ 2014-05-08 19:52 ` Randy Brukardt 1 sibling, 0 replies; 94+ messages in thread From: Randy Brukardt @ 2014-05-08 19:52 UTC (permalink / raw) "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. ^ permalink raw reply [flat|nested] 94+ messages in thread
* Re: Safety of unprotected concurrent operations on constant objects 2014-05-06 6:00 ` Brad Moore 2014-05-06 8:11 ` Dmitry A. Kazakov @ 2014-05-06 16:22 ` Robert A Duff 2014-05-06 19:07 ` Dmitry A. Kazakov 1 sibling, 1 reply; 94+ messages in thread From: Robert A Duff @ 2014-05-06 16:22 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 94+ messages in thread
* Re: Safety of unprotected concurrent operations on constant objects 2014-05-06 16:22 ` Robert A Duff @ 2014-05-06 19:07 ` Dmitry A. Kazakov 2014-05-08 5:03 ` Brad Moore 0 siblings, 1 reply; 94+ messages in thread From: Dmitry A. Kazakov @ 2014-05-06 19:07 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 94+ messages in thread
* Re: Safety of unprotected concurrent operations on constant objects 2014-05-06 19:07 ` Dmitry A. Kazakov @ 2014-05-08 5:03 ` Brad Moore 2014-05-08 12:03 ` Brad Moore 0 siblings, 1 reply; 94+ messages in thread From: Brad Moore @ 2014-05-08 5:03 UTC (permalink / raw) 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. ^ permalink raw reply [flat|nested] 94+ messages in thread
* Re: Safety of unprotected concurrent operations on constant objects 2014-05-08 5:03 ` Brad Moore @ 2014-05-08 12:03 ` Brad Moore 2014-05-08 19:57 ` Randy Brukardt 0 siblings, 1 reply; 94+ messages in thread From: Brad Moore @ 2014-05-08 12:03 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 94+ messages in thread
* Re: Safety of unprotected concurrent operations on constant objects 2014-05-08 12:03 ` Brad Moore @ 2014-05-08 19:57 ` Randy Brukardt 2014-05-09 2:58 ` Brad Moore 0 siblings, 1 reply; 94+ messages in thread From: Randy Brukardt @ 2014-05-08 19:57 UTC (permalink / raw) "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. ^ permalink raw reply [flat|nested] 94+ messages in thread
* Re: Safety of unprotected concurrent operations on constant objects 2014-05-08 19:57 ` Randy Brukardt @ 2014-05-09 2:58 ` Brad Moore 0 siblings, 0 replies; 94+ messages in thread From: Brad Moore @ 2014-05-09 2:58 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 94+ messages in thread
* Re: Safety of unprotected concurrent operations on constant objects 2014-05-05 15:11 ` Brad Moore 2014-05-05 16:36 ` Dmitry A. Kazakov @ 2014-05-05 20:29 ` Natasha Kerensikova 2014-05-08 3:41 ` Randy Brukardt 1 sibling, 1 reply; 94+ messages in thread From: Natasha Kerensikova @ 2014-05-05 20:29 UTC (permalink / raw) 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? ^ permalink raw reply [flat|nested] 94+ messages in thread
* Re: Safety of unprotected concurrent operations on constant objects 2014-05-05 20:29 ` Natasha Kerensikova @ 2014-05-08 3:41 ` Randy Brukardt 2014-05-08 9:07 ` Natasha Kerensikova 0 siblings, 1 reply; 94+ messages in thread From: Randy Brukardt @ 2014-05-08 3:41 UTC (permalink / raw) "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. ^ permalink raw reply [flat|nested] 94+ messages in thread
* Re: Safety of unprotected concurrent operations on constant objects 2014-05-08 3:41 ` Randy Brukardt @ 2014-05-08 9:07 ` Natasha Kerensikova 2014-05-08 19:35 ` Randy Brukardt 0 siblings, 1 reply; 94+ messages in thread From: Natasha Kerensikova @ 2014-05-08 9:07 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 94+ messages in thread
* Re: Safety of unprotected concurrent operations on constant objects 2014-05-08 9:07 ` Natasha Kerensikova @ 2014-05-08 19:35 ` Randy Brukardt 0 siblings, 0 replies; 94+ messages in thread From: Randy Brukardt @ 2014-05-08 19:35 UTC (permalink / raw) "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. ^ permalink raw reply [flat|nested] 94+ messages in thread
* Re: Safety of unprotected concurrent operations on constant objects 2014-05-05 8:39 ` Simon Wright 2014-05-05 15:11 ` Brad Moore @ 2014-05-08 3:12 ` Randy Brukardt 1 sibling, 0 replies; 94+ messages in thread From: Randy Brukardt @ 2014-05-08 3:12 UTC (permalink / raw) "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. ^ permalink raw reply [flat|nested] 94+ messages in thread
* Re: Safety of unprotected concurrent operations on constant objects 2014-05-04 21:44 ` Shark8 2014-05-05 8:39 ` Simon Wright @ 2014-05-05 22:30 ` Brad Moore 1 sibling, 0 replies; 94+ messages in thread From: Brad Moore @ 2014-05-05 22:30 UTC (permalink / raw) 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. ^ permalink raw reply [flat|nested] 94+ messages in thread
* Re: Safety of unprotected concurrent operations on constant objects 2014-05-04 15:18 ` sbelmont700 2014-05-04 15:57 ` Natasha Kerensikova @ 2014-05-04 16:04 ` Peter Chapin 2014-05-04 18:07 ` Natasha Kerensikova 1 sibling, 1 reply; 94+ messages in thread From: Peter Chapin @ 2014-05-04 16:04 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 94+ messages in thread
* Re: Safety of unprotected concurrent operations on constant objects 2014-05-04 16:04 ` Peter Chapin @ 2014-05-04 18:07 ` Natasha Kerensikova 0 siblings, 0 replies; 94+ messages in thread From: Natasha Kerensikova @ 2014-05-04 18:07 UTC (permalink / raw) 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... ^ permalink raw reply [flat|nested] 94+ messages in thread
* Re: Safety of unprotected concurrent operations on constant objects 2014-05-04 7:46 ` Natasha Kerensikova 2014-05-04 8:06 ` Dmitry A. Kazakov 2014-05-04 15:18 ` sbelmont700 @ 2014-05-04 18:55 ` Jeffrey Carter 2014-05-04 19:36 ` Simon Wright 2014-05-05 22:46 ` Brad Moore 2014-05-04 20:25 ` Shark8 3 siblings, 2 replies; 94+ messages in thread From: Jeffrey Carter @ 2014-05-04 18:55 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 94+ messages in thread
* Re: Safety of unprotected concurrent operations on constant objects 2014-05-04 18:55 ` Jeffrey Carter @ 2014-05-04 19:36 ` Simon Wright 2014-05-04 20:29 ` Jeffrey Carter 2014-05-05 22:46 ` Brad Moore 1 sibling, 1 reply; 94+ messages in thread From: Simon Wright @ 2014-05-04 19:36 UTC (permalink / raw) 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! ^ permalink raw reply [flat|nested] 94+ messages in thread
* Re: Safety of unprotected concurrent operations on constant objects 2014-05-04 19:36 ` Simon Wright @ 2014-05-04 20:29 ` Jeffrey Carter 0 siblings, 0 replies; 94+ messages in thread From: Jeffrey Carter @ 2014-05-04 20:29 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 94+ messages in thread
* Re: Safety of unprotected concurrent operations on constant objects 2014-05-04 18:55 ` Jeffrey Carter 2014-05-04 19:36 ` Simon Wright @ 2014-05-05 22:46 ` Brad Moore 1 sibling, 0 replies; 94+ messages in thread From: Brad Moore @ 2014-05-05 22:46 UTC (permalink / raw) 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. ^ permalink raw reply [flat|nested] 94+ messages in thread
* Re: Safety of unprotected concurrent operations on constant objects 2014-05-04 7:46 ` Natasha Kerensikova ` (2 preceding siblings ...) 2014-05-04 18:55 ` Jeffrey Carter @ 2014-05-04 20:25 ` Shark8 2014-05-04 23:33 ` sbelmont700 2014-05-05 7:38 ` Dmitry A. Kazakov 3 siblings, 2 replies; 94+ messages in thread From: Shark8 @ 2014-05-04 20:25 UTC (permalink / raw) 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; ^ permalink raw reply [flat|nested] 94+ messages in thread
* Re: Safety of unprotected concurrent operations on constant objects 2014-05-04 20:25 ` Shark8 @ 2014-05-04 23:33 ` sbelmont700 2014-05-05 7:38 ` Dmitry A. Kazakov 1 sibling, 0 replies; 94+ messages in thread From: sbelmont700 @ 2014-05-04 23:33 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 94+ messages in thread
* Re: Safety of unprotected concurrent operations on constant objects 2014-05-04 20:25 ` Shark8 2014-05-04 23:33 ` sbelmont700 @ 2014-05-05 7:38 ` Dmitry A. Kazakov 2014-05-08 3:45 ` Randy Brukardt 1 sibling, 1 reply; 94+ messages in thread From: Dmitry A. Kazakov @ 2014-05-05 7:38 UTC (permalink / raw) 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 ^ permalink raw reply [flat|nested] 94+ messages in thread
* Re: Safety of unprotected concurrent operations on constant objects 2014-05-05 7:38 ` Dmitry A. Kazakov @ 2014-05-08 3:45 ` Randy Brukardt 0 siblings, 0 replies; 94+ messages in thread From: Randy Brukardt @ 2014-05-08 3:45 UTC (permalink / raw) "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. ^ permalink raw reply [flat|nested] 94+ messages in thread
* Re: Safety of unprotected concurrent operations on constant objects 2014-05-02 8:42 Safety of unprotected concurrent operations on constant objects Natasha Kerensikova 2014-05-03 13:43 ` sbelmont700 @ 2014-05-08 3:19 ` Randy Brukardt 1 sibling, 0 replies; 94+ messages in thread From: Randy Brukardt @ 2014-05-08 3:19 UTC (permalink / raw) "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. ^ permalink raw reply [flat|nested] 94+ messages in thread
end of thread, other threads:[~2014-10-26 17:11 UTC | newest] Thread overview: 94+ messages (download: mbox.gz / follow: Atom feed) -- links below jump to the message on this page -- 2014-05-02 8:42 Safety of unprotected concurrent operations on constant objects Natasha Kerensikova 2014-05-03 13:43 ` sbelmont700 2014-05-03 20:54 ` Natasha Kerensikova 2014-05-03 21:40 ` Simon Wright 2014-05-04 0:28 ` Jeffrey Carter 2014-05-04 7:46 ` Natasha Kerensikova 2014-05-04 8:06 ` Dmitry A. Kazakov 2014-05-04 15:18 ` sbelmont700 2014-05-04 15:57 ` Natasha Kerensikova 2014-05-04 18:30 ` sbelmont700 2014-05-04 19:34 ` Dmitry A. Kazakov 2014-05-05 19:04 ` Brad Moore 2014-05-05 21:23 ` Brad Moore 2014-05-04 21:44 ` Shark8 2014-05-05 8:39 ` Simon Wright 2014-05-05 15:11 ` Brad Moore 2014-05-05 16:36 ` Dmitry A. Kazakov 2014-05-06 6:00 ` Brad Moore 2014-05-06 8:11 ` Dmitry A. Kazakov 2014-05-06 8:48 ` Alejandro R. Mosteo 2014-05-06 9:49 ` G.B. 2014-05-06 12:19 ` Dmitry A. Kazakov 2014-05-06 12:58 ` G.B. 2014-05-06 15:00 ` Dmitry A. Kazakov 2014-05-06 16:24 ` G.B. 2014-05-06 19:14 ` Dmitry A. Kazakov 2014-05-07 6:49 ` Georg Bauhaus 2014-05-07 7:40 ` Dmitry A. Kazakov 2014-05-07 11:25 ` G.B. 2014-05-07 12:14 ` Dmitry A. Kazakov 2014-05-07 13:45 ` G.B. 2014-05-07 14:08 ` Dmitry A. Kazakov 2014-05-07 17:45 ` Simon Wright 2014-05-07 18:28 ` Georg Bauhaus 2014-05-07 4:59 ` J-P. Rosen 2014-05-07 7:30 ` Dmitry A. Kazakov 2014-05-07 8:26 ` J-P. Rosen 2014-05-07 9:09 ` Dmitry A. Kazakov 2014-05-07 11:29 ` J-P. Rosen 2014-05-07 12:36 ` Safety of unprotected concurrent operations on constant objects (was: Safety of unprotected concurrent operations on constant objects) Dmitry A. Kazakov 2014-05-07 14:04 ` Safety of unprotected concurrent operations on constant objects G.B. 2014-05-08 4:12 ` Brad Moore 2014-05-08 8:20 ` Dmitry A. Kazakov 2014-05-08 10:30 ` G.B. 2014-05-09 13:14 ` Brad Moore 2014-05-09 19:00 ` Dmitry A. Kazakov 2014-05-10 12:30 ` Brad Moore 2014-05-10 20:27 ` Dmitry A. Kazakov 2014-05-11 6:56 ` Brad Moore 2014-05-11 18:01 ` Brad Moore 2014-05-12 8:13 ` Dmitry A. Kazakov 2014-05-13 4:50 ` Brad Moore 2014-05-13 8:56 ` Dmitry A. Kazakov 2014-05-13 15:01 ` Brad Moore 2014-05-13 15:38 ` Brad Moore 2014-05-13 16:46 ` Simon Wright 2014-05-13 19:15 ` Dmitry A. Kazakov 2014-05-13 16:08 ` Dmitry A. Kazakov 2014-05-13 20:27 ` Randy Brukardt 2014-05-14 4:30 ` Shark8 2014-05-14 21:37 ` Randy Brukardt 2014-05-14 21:56 ` Robert A Duff 2014-05-15 1:21 ` Shark8 2014-05-14 14:30 ` Brad Moore 2014-05-15 8:03 ` Dmitry A. Kazakov 2014-05-15 13:21 ` Robert A Duff 2014-05-15 14:27 ` Dmitry A. Kazakov 2014-05-15 15:53 ` Robert A Duff 2014-05-15 16:30 ` Dmitry A. Kazakov 2014-10-26 17:11 ` Jacob Sparre Andersen 2014-05-08 19:52 ` Randy Brukardt 2014-05-06 16:22 ` Robert A Duff 2014-05-06 19:07 ` Dmitry A. Kazakov 2014-05-08 5:03 ` Brad Moore 2014-05-08 12:03 ` Brad Moore 2014-05-08 19:57 ` Randy Brukardt 2014-05-09 2:58 ` Brad Moore 2014-05-05 20:29 ` Natasha Kerensikova 2014-05-08 3:41 ` Randy Brukardt 2014-05-08 9:07 ` Natasha Kerensikova 2014-05-08 19:35 ` Randy Brukardt 2014-05-08 3:12 ` Randy Brukardt 2014-05-05 22:30 ` Brad Moore 2014-05-04 16:04 ` Peter Chapin 2014-05-04 18:07 ` Natasha Kerensikova 2014-05-04 18:55 ` Jeffrey Carter 2014-05-04 19:36 ` Simon Wright 2014-05-04 20:29 ` Jeffrey Carter 2014-05-05 22:46 ` Brad Moore 2014-05-04 20:25 ` Shark8 2014-05-04 23:33 ` sbelmont700 2014-05-05 7:38 ` Dmitry A. Kazakov 2014-05-08 3:45 ` Randy Brukardt 2014-05-08 3:19 ` Randy Brukardt
This is a public inbox, see mirroring instructions for how to clone and mirror all data and code used for this inbox