Unformatted version of **ai12s/ai12-0321-1.txt version 1.6**

Other versions for file**ai12s/ai12-0321-1.txt**

Other versions for file

!standard C.6.3(0) 19-03-11 AI12-0321-1/03

!standard C.6.4(0)

!class Amendment 19-03-07

!status Amendment 1-2012 19-03-11

!status ARG Approved 9-0-1 19-03-11

!status work item 19-03-07

!status received 19-03-07

!priority Low

!difficulty Easy

!subject Support for Arithmetic Atomic Operations and Test and Set

!standard C.6.4(0)

!class Amendment 19-03-07

!status Amendment 1-2012 19-03-11

!status ARG Approved 9-0-1 19-03-11

!status work item 19-03-07

!status received 19-03-07

!priority Low

!difficulty Easy

!subject Support for Arithmetic Atomic Operations and Test and Set

!summary

!problem

On multiprocessor platforms, relying on locks for synchronization can be
problematic. One issue is that while a task is blocked, it can be difficult or
impossible to offer guarantees for progress. Other problems associated with
locks includes deadlock, livelock, and priority inversion. Locking can also be a
significant detriment to performance, and reduce opportunities for parallelism.

Lock-free data structures guarantee system-wide progress, while wait-free data
structures, in addition to being lock-free, also guarantee per-thread progresss.

Lock-free data structures can also be used to improve performance by increasing
the amount of time spent executing in parallel since access to the data
structure does not need to be serialised.

AI12-0234-1 provides access to swap and compare-and-swap operations, but there
are other useful operations that could be provided as atomic primitives.

Atomic arithmetic, such as being able to atomically increment an atomic
counter is a common use for atomic operations. Another common need in this
area is to create spin-locks in user space via test and set instructions.

Ada should provide some simple primitives that can be mapped to hardware
instructions that allow such updates to perform as expected.

!proposal

This proposal depends on AI12-0234-1, which defines the parent package
Ada.Atomic_Operations.

The solution is to provide a set of standard library calls that map to commonly
available atomic hardware instructions such as test and set, and atomic
increment. These subprograms are to be intrinsic calls.

The libraries are generic libraries in order to support operations on discrete
types of different sizes, and we require that the actual types for the generics
be atomic types, so that Ada's semantics of atomic types can be associated
with these primitive operations.

!wording

C.6.3 The Package System.Atomic_Operations.Test_And_Set

The language-defined package System.Atomic_Operations.Test_And_Set
provides an operation to atomically set and clear an atomic flag object.

Static Semantics

The library package System.Atomic_Operations.Test_And_Set has the
following declaration:

Test_And_Set_Flag represents the state of an atomic flag object.
An atomic flag object can either be considered to be set or cleared.

Atomic_Test_And_Set performs an atomic test-and-set operation on Item.
Item is set to some implementation-defined nonzero value. The function returns
True if the previous contents were nonzero, and otherwise returns False.

Atomic_Clear performs an atomic clear operation on Item. After the
operation, Item contains 0. This call should be used in conjunction with
Atomic_Test_And_Set.

C.6.4 The Package System.Atomic_Operations.Arithmetic

The language-defined generic package System.Atomic_Operations.Arithmetic
provides operations to perform arithmetic atomically on objects of
integer types.

Static Semantics

The generic library package System.Atomic_Operations.Arithmetic has the
following declaration:

The operations of this package are defined as follows:

Atomically performs: Item := Item + Value;

Atomically performs: Item := Item - Value;

Atomically performs: Tmp := Item; Item := Item + Value; return Tmp;

Atomically performs: Tmp := Item; Item := Item - Value; return Tmp;

!discussion

The approach taken to improving support for lock free data structures is to
provide a set of libraries of low level atomic primitives similar to the library
that is provided by gcc for C and C++.

The library of intrinsic primitives might be of interest to those wishing to
implement specific lock free algorithms, particularly if porting those applications
from other languages.

It was considered whether modular arithmetic functions should be provided.
While it is possible, the routines would be trickier to write because
in the cases where the modulus of the modular types is not a multiple of
System.Storage_Unit. For such cases, updating an atomic variable might
need to include a write back to the the atomic variable to handle the
wrap around. With signed arithmetic, we need to generate Constraint_Error
for overflow checks, so checking for overflow is needed. But if
extra performance is needed, those checks can be suppressed.

!corrigendum C.6.3

Insert new clause:

The language-defined package System.Atomic_Operations.Test_And_Set
provides an operation to atomically set and clear an atomic flag object.

The library package System.Atomic_Operations.Test_And_Set has the
following declaration:

Test_And_Set_Flag represents the state of an atomic flag object.
An atomic flag object can either be considered to be set or cleared.

Atomic_Test_And_Set performs an atomic test-and-set operation on Item.
Item is set to some implementation-defined nonzero value. The function returns
True if the previous contents were nonzero, and otherwise returns False.

Atomic_Clear performs an atomic clear operation on Item. After the
operation, Item contains 0. This call should be used in conjunction with
Atomic_Test_And_Set.

!corrigendum C.6.4

Insert new clause:

The language-defined generic package System.Atomic_Operations.Arithmetic
provides operations to perform arithmetic atomically on objects of
integer types.

The generic library package System.Atomic_Operations.Arithmetic has the
following declaration:

The operations of this package are defined as follows:

Atomically performs: Item := Item + Value;

Atomically performs: Item := Item - Value;

Atomically performs: Tmp := Item; Item := Item + Value; **return** Tmp;

Atomically performs: Tmp := Item; Item := Item - Value; **return** Tmp;

!ASIS

No ASIS effect.

!ACATS test

An ACATS C-Test is needed to check that the new capabilities are supported.

!appendix

From: Brad Moore Sent: Thursday, March 07, 2019 6:03 PM Here is my first draft for a new AI on additional atomic operations. This content was split off from AI12-0234-1. [This is version /01 of this AI - Editor.] I eliminated functions that did not seem to be needed, such as atomic load, atomic store, and atomic fences. I also eliminated the signed arithmetic package. The modular arithmetic better maps to the underlying calls, since the signed onces would need to support detection of arithmetic overflow, which the underlying gcc instrinsic functions do not do. We could add signed arithmetic functions in the future if the need was great enough. **************************************************************** From: Brad Moore Sent: Saturday, March 09, 2019 1:51 PM Here is an update to AI12-0321-1 [This is version /02 of the AI - Editor.] The main changes are; - Atomic_Exchange was pulled out of this AI, and moved to AI12-234-1 - The child packages of Atomic_Operations, are rooted under package System, rather than package Ada. - Wording was moved to follow section C.6, Shared Variable Control - The functions of the form Atomic_xxx_And_Fetch were removed. The C standard only defines Atomic_Fetch_And_xxx functions, and it didn't seem like it was worth providing both forms. - The following procedures were added to Atomic_Operations.Arithmetic procedure Atomic_Add (Item : aliased in out Atomic_Type; Value : Atomic_Type) with Convention => Intrinsic; procedure Atomic_Subtract (Item : aliased in out Atomic_Type; Value : Atomic_Type) with Convention => Intrinsic; procedure Atomic_Bitwise_And (Item : aliased in out Atomic_Type; Value : Atomic_Type) with Convention => Intrinsic; procedure Atomic_Bitwise_Or (Item : aliased in out Atomic_Type; Value : Atomic_Type) with Convention => Intrinsic; procedure Atomic_Xor (Item : aliased in out Atomic_Type; Value : Atomic_Type) with Convention => Intrinsic; This is because all the other functions return the original value before the operation was applied, and in many cases, the user will not need these values. This can simplify the implementation of the calls, and more optimal performance. - The call function Atomic_Fetch_And_Nand (Item : aliased in out Atomic_Type; Value : Atomic_Type) return Atomic_Type with Intrinsic; Was removed. The C11 standard does not define this function, and it doesn't seem likely that there is a great need to perform atomic nands. If such a need materializes, we could add it in the future. - Is_Lock_Free was added to the Test_And_Set child package and the Arithmetic child package. - The generic formal type for the Atomic_Operations.Arithmetic package was changed from a modular generic formal type to a signed arithmetic generic formal type. This is because it was perceived that supporting atomic updates for modular types where the modulus is not a multiple of the storage unit, is trickier, and possibly requiring loops involving compare and swap. Using signed arithmetic means there is a need to check for arithmetic overflow, but that can be done without looping, and if performance is an issue, the overflow checks can be suppressed. **************************************************************** From: Brad Moore Sent: Wednesday, March 13, 2019 12:22 AM In the recent electronic ARG meeting, we were discussing the Atomic_Operations.Arithmetic package. It was mentioned that the Bitwise operations that were defined in AI12-0321-1 did not make sense if the generic formal type is a signed integer type, so we decided to drop those subprograms from the AI. The thought was that Atomic Addition and Subtraction is likely the most common need to support, and that Bitwise operations seemed to be much less of a need. I mentioned that prior to Saturday, the generic formal of the Arithmetic package was a modular type, but that I had changed it to signed integer, due to perceived issues with dealing with addition and subtraction, when the modulus of the generic formal type was not a multiple of the machines storage element size. The decision to have the Arithmetic package only support the Add and Subtract, still makes sense to me. But I am now thinking we were a bit too hasty in tossing out the bitwise subprograms. After thinking about it, I think atomically modifying and testing bits atomically is probably something that could be quite useful. Something I might have used for example, in my Paraffin libraries. If we wanted to support atomic bitwise operations, I think we'd want to limit the support to modular types whose modulus is a power of two. That way, one cannot get into trouble setting or clearing bits of the generic formal modular type. All bit patterns (for values less than the 2**modulus) are valid bit patterns, so there would be no need to add additional checks on the results of these operations. Fortunately, that restriction could easily be enforced by placing the following assert in the generic package. -- Only Modular types whose modulus is a power of 2 are allowed pragma Assert ((Atomic_Type'Base (Atomic_Type'Modulus) and Atomic_Type'Base (Atomic_Type'Modulus - 1)) = 0); Since adding these functions would be very similar to the wording for adding the Atomic_Operations.Arithmetic package, I think we should consider adding the following which supports three operations, "or", "and", and "xor"; generic type Atomic_Type is mod <> with Atomic; package System.Atomic_Operations.Bitwise with Pure, Nonblocking is -- Only Modular types whose modulus is a power of 2 are allowed pragma Assert ((Atomic_Type'Base (Atomic_Type'Modulus) and Atomic_Type'Base (Atomic_Type'Modulus - 1)) = 0); procedure Atomic_Bitwise_And (Item : aliased in out Atomic_Type; Value : Atomic_Type) with Convention => Intrinsic; procedure Atomic_Bitwise_Or (Item : aliased in out Atomic_Type; Value : Atomic_Type) with Convention => Intrinsic; procedure Atomic_Bitwise_Xor (Item : aliased in out Atomic_Type; Value : Atomic_Type) with Convention => Intrinsic; function Atomic_Fetch_And_Bitwise_And (Item : aliased in out Atomic_Type; Value : Atomic_Type) return Atomic_Type with Convention => Intrinsic; function Atomic_Fetch_And_Bitwise_Or (Item : aliased in out Atomic_Type; Value : Atomic_Type) return Atomic_Type with Convention => Intrinsic; function Atomic_Fetch_And_Bitwise_Xor (Item : aliased in out Atomic_Type; Value : Atomic_Type) return Atomic_Type with Convention => Intrinsic; function Is_Lock_Free (Item : aliased Atomic_Type) return Boolean with Convention => Intrinsic, Nonblocking end System.Atomic_Operations.Bitwise; I'd be happy to write this up (likely as a new AI if it cant be added to AI12-0321-1. Thoughts? *************************************************************** From: Randy Brukardt Sent: Wednesday, March 13, 2019 12:49 AM ... > Fortunately, that restriction could easily be enforced by placing the > following assert in the generic package. > > -- Only Modular types whose modulus is a power of 2 are allowed > pragma Assert ((Atomic_Type'Base (Atomic_Type'Modulus) and > Atomic_Type'Base (Atomic_Type'Modulus - 1)) = 0); I think this Assertion always raises Constraint_Error (or is illegal). Atomic_Type'Modulus is a universal_integer value, and those do not wrap. For all T, T'Modulus > T'Last. Ergo, T'Modulus is out of range. If T'Modulus was static (as it might be in an instance), then the type conversion is illegal. You need to somehow use 'Mod. However, T'Mod(T'Modulus) is always 0. I've usually had to declare a Big_Mod type for this sort of thing: type Big_Mod is mod System.Max_Binary_Modulus; and then you can write your expression, so long as you pretest for modulii that are too large. Which is a royal mess. :-) Anyway, you need to go back to the drawing board with this assertion. **************************************************************** From: Brad Moore Sent: Wednesday, March 13, 2019 1:32 AM > I think this Assertion always raises Constraint_Error (or is illegal). > Atomic_Type'Modulus is a universal_integer value, and those do not > wrap. For all T, T'Modulus > T'Last. Ergo, T'Modulus is out of range. > If T'Modulus was static (as it might be in an instance), then the type > conversion is illegal. I knew that Atomic_Type'Modulus is a universal_integer value, which is why I converted that result to the Atomic_Type'Base subtype, which allows me to do the bitwise and operation. I tried this with GNAT, and it compiles, and works fine in my test program. When I try it with a type such as type Mod_5 is mod 5; It correctly tells me that an exception will be raised at runtime. (since the modulus of that subtype is not a power of 2) **************************************************************** From: Tucker Taft Sent: Wednesday, March 13, 2019 8:40 AM In any case, I think we should leave these out for now, as they are less critical than add/subtract. It is easy enough to write such a package yourself if you know what you are doing. Here we are looking for widely useful capabilities that need standardization. **************************************************************** From: Randy Brukardt Sent: Wednesday, March 13, 2019 3:41 PM > I knew that Atomic_Type'Modulus is a universal_integer value, which is > why I converted that result to the Atomic_Type'Base subtype, which > allows me to do the bitwise and operation. Yes, and that conversion always raises Constraint_Error (or is illegal if the type is static). > I tried this with GNAT, and it compiles, and works fine in my test > program. Either you didn't actually test what you think you did, or GNAT is wrong. 4.6(28) clearly states that Constraint_Error is raised for a value outside of the base range of a modular type. T'Modulus is by definition outside of the base range of T. And 4.9 states that a static expression is illegal if it raises any exception other than an overflow. Now, I know that if you compiled this with Janus/Ada, it would in fact work with at least some types, but that would be because Janus/Ada doesn't properly handle these conversions when found in a generic. In particular, T'Modulus of mod 2**32 has the special value zero at runtime so we can handle such types correctly, but that would of course cause oddities if actually used explicitly. But just because it would work doesn't make it right. So I wouldn't be surprised if it accidentally worked for Max_Binary_Modulus, but I wouldn't take that as some sort of assumption that it should work. I'd suggest trying it in a non-generic case to see. I'm pretty sure that there is an ACATS test that checks this rule, but perhaps it could use some beefing up. > When I try it with a type such as > > type Mod_5 is mod 5; > > It correctly tells me that an exception will be raised at runtime. > (since the modulus of that subtype is not a power of 2) Surely this is true, since it *always* raises Constraint_Error. **************************************************************** From: Tucker Taft Sent: Wednesday, March 13, 2019 4:30 PM Another test that should work, I believe, is: pragma Assert (T'Modulus = 2 ** T'Size); unless the 'Size has been explicitly specified to be larger. Or if you want to go whole hog: pragma Assert((for some I in 1..T'Size => T'Modulus = 2**I)); though now you are getting into non-static expressions, so Constraint_Error becomes more likely if you bump up against the Max_Integer limits of run-time universal-int computations. ;-) **************************************************************** From: Bob Duff Sent: Wednesday, March 13, 2019 6:00 PM > pragma Assert((for some I in 1..T'Size => T'Modulus = 2**I)); For "type T is mod 1;", T'Size = 0, 2**T'Size = 1, and T'Modulus = 1. ;-) Note to Brad: Unlike signed integers, the base range of a modular type is widened beyond the first subtype. **************************************************************** From: Tucker Taft Sent: Wednesday, March 13, 2019 7:27 PM Yes, I realized that, but I was somehow unable to allow myself to include the "mod 1" option. ;-) **************************************************************** From: Tucker Taft Sent: Wednesday, March 13, 2019 7:33 PM > Note to Brad: Unlike signed integers, the base range of a modular > type is widened beyond the first subtype. What does this mean? Did you mean the base range is *not* widened? **************************************************************** From: Bob Duff Sent: Wednesday, March 13, 2019 8:12 PM Yes, thanks for the correction. **************************************************************** From: Brad Moore Sent: Wednesday, March 13, 2019 11:30 PM Thanks for the explanations. By the way, the reason I thought the following example was OK, is because I didn't have the "enable assertions" checkbox checked, for the project file. Oddly, I do get a warning if I uncomment the assert below, which says that an assertion would fail at run time. But I don't get any warnings otherwise, and the code runs successfully. If I enable assertions, then the code does not compile, as Randy said. with Ada.Text_IO; use Ada.Text_IO; procedure Main is type Mod_8 is mod 2**3; type Mod_5 is mod 5; type Mod_16 is mod 2**4; type Mod_32 is mod 2**5; pragma Assert ((Mod_8'Base (Mod_8'Modulus) and Mod_8'Base (Mod_8'Modulus - 1)) = 0); pragma Assert ((Mod_16'Base (Mod_16'Modulus) and Mod_16'Base (Mod_16'Modulus - 1)) = 0); pragma Assert ((Mod_32'Base (Mod_32'Modulus) and Mod_32'Base (Mod_32'Modulus - 1)) = 0); -- pragma Assert (((Mod_5'Base (Mod_5'Modulus) and -- Mod_5'Base (Mod_5'Modulus - 1)) = 0)); X : Mod_8; X2 : Mod_16; X3 : Mod_32; begin X := 4; X := X + 7; X2 := 4; X2 := X2 + 14; X3 := 5; X3 := X3 + 30; Put_Line ("Mod8:" & Mod_8'Image (X)); Put_Line ("Mod16:" & Mod_16'Image (X2)); Put_Line ("Mod32:" & Mod_32'Image (X3)); end Main; **************************************************************** From: Brad Moore Sent: Wednesday, March 13, 2019 11:39 PM Thanks for the suggestion, that works (the first simpler version, at least) for my example. A nice concise way to express this property. **************************************************************** From: Randy Brukardt Sent: Thursday, March 14, 2019 7:21 PM > > pragma Assert((for some I in 1..T'Size => T'Modulus = 2**I)); > > For "type T is mod 1;", T'Size = 0, 2**T'Size = 1, and T'Modulus = 1. > > ;-) Tucker noted that it isn't a very good assertion, since someone could declare: type Biggie is mod 256 with Atomic, Size => 16; OTOH, we could decide to explicitly not care about such corner cases. > Note to Brad: Unlike signed integers, the base range of a modular > type is widened beyond the first subtype. Every time I read this, I'm confused. I even went and looked it up in the RM to be sure. I think there is a "not" missing somewhere. Perhaps you meant: Note to Brad: Unlike signed integers, the base range of a modular type is NOT widened beyond the first subtype. **************************************************************** From: Brad Moore Sent: Sunday, March 17, 2019 10:56 AM >> >> > pragma Assert((for some I in 1..T'Size => T'Modulus = 2**I)); >> >> For "type T is mod 1;", T'Size = 0, 2**T'Size = 1, and T'Modulus = 1. >> >> ;-) > > Tucker noted that it isn't a very good assertion, since someone could > declare: > > type Biggie is mod 256 with Atomic, Size => 16; > > OTOH, we could decide to explicitly not care about such corner cases. Given the choice in this case, I think it's probably better to have an assertion that always works, rather than one that mostly works, even if it is a bit more expensive. At least the assertion if enabled is only applied during generic instantiation. To address Bob's comment, it doesn't make sense to have bitwise operations on a type that doesn't have any bits, so I would extend the assertion to; pragma Assert(T'Modulus > 1 and (for some I in 1..T'Size => T'Modulus = 2**I)); In this case, it's too bad that Ada hadn't defined a nand keyword similar to xor which could be used for logical or bitwise operations. That could be used to get the ones complement of any modular type. Currently, we have the "not" keyword, but that only gives you a ones complement if the modulus of the type is binary. If we had that, then we could write instead; pragma Assert((T'Last nand T'Last) = 0); >> Note to Brad: Unlike signed integers, the base range of a modular >> type is widened beyond the first subtype. > > Every time I read this, I'm confused. I even went and looked it up in > the RM to be sure. I think there is a "not" missing somewhere. Perhaps you meant: > > Note to Brad: Unlike signed integers, the base range of a > modular type is NOT widened beyond the first subtype. Bob later clarified that he had meant to put the NOT in. **************************************************************** From: Randy Brukardt Sent: Monday, March 18, 2019 10:19 PM > To address Bob's comment, it doesn't make sense to have bitwise > operations on a type that doesn't have any bits, so I would extend the > assertion to; > > pragma Assert(T'Modulus > 1 and (for some I in 1..T'Size => T'Modulus > = 2**I)); You probably need to guard against overflow when T'Modulus = System.Max_Binary_Modulus, which is probably bigger than root_integer'Last (which is a signed integer type). And this will be evaluated using root_integer, since it is a universal_integer expression that isn't static. Moreover, you don't need the pretest, since the quantified expression doesn't allow T'Modulus = 1 (2**1 being 2, last I checked :-). Ergo: pragma Assert(T'Modulus = System.Max_Binary_Modulus or else (for some I in 1..T'Size => T'Modulus = 2**I); As written, this will still overflow on a machine with a 32-bit root_integer for something like: type Funny is mod 7 with Atomic, Size => 32; but this is truly weird, and the assertion would fail anyway for Funny -- not sure it's worth ensuring a particular exception in this case (that is, Assertion_Error vs. Constraint_Error). [And of course, change 32 to whatever the size of root_integer is, this will fail on any machine unless it doesn't support maximum integer-sized atomics -- which seems unlikely.] ... > If we had that, then we could write instead; > > pragma Assert((T'Last nand T'Last) = 0); Tricky! We probably want the assertion to be understandable to the relatively causal reader, and this is not that. (Otherwise, we'd have to repeat it in English so people know what they're allowed to do, which defeats the point.) **************************************************************** From: Tucker Taft Sent: Tuesday, March 19, 2019 3:59 AM In any case, I would separate this from the arithmetic operations, and probably put it in a separate AI, that I at least would suggest deferring for now. **************************************************************** From: Brad Moore Sent: Friday, March 22, 2019 12:25 AM >> To address Bob's comment, it doesn't make sense to have bitwise >> operations on a type that doesn't have any bits, so I would extend >> the assertion to; >> >> pragma Assert(T'Modulus > 1 and (for some I in 1..T'Size => T'Modulus >> = 2**I)); > > You probably need to guard against overflow when T'Modulus = > System.Max_Binary_Modulus, which is probably bigger than > root_integer'Last (which is a signed integer type). And this will be > evaluated using root_integer, since it is a universal_integer expression > that isn't static. Right, but what I had to do to get this to work involved jumping through a rather extraordinary number of hoops. See below.... > Moreover, you don't need the pretest, since the quantified expression > doesn't allow T'Modulus = 1 (2**1 being 2, last I checked :-). Right. Ergo: > > pragma Assert(T'Modulus = System.Max_Binary_Modulus or else > (for some I in 1..T'Size => T'Modulus = 2**I); > > As written, this will still overflow on a machine with a 32-bit > root_integer for something like: > type Funny is mod 7 with Atomic, Size => 32; but this is truly > weird, and the assertion would fail anyway for Funny -- not sure it's > worth ensuring a particular exception in this case (that is, > Assertion_Error vs. Constraint_Error). > > [And of course, change 32 to whatever the size of root_integer is, > this will fail on any machine unless it doesn't support maximum > integer-sized atomics which seems unlikely.] This works ordinarily, but doesn't work for a generic formal modular type. Or at least it doesn't in GNAT. I get the following warnings for the compilation if I prepend the expression Atomic_Type'Modulus = System.Max_Binary_Modulus or else atomic_operations-bitwise.ads:9:47: warning: non-static universal integer value out of range atomic_operations-bitwise.ads:9:47: warning: "Constraint_Error" will be raised at run time This makes sense to me, as the generic doesn't know that its actual type wont have a non-binary modulus. I suspect an assume-the-worst rule is being applied here. The limit for a non-binary modulus as defined in System.Max_Nonbinary_Modulus on GNAT is 2 ** Integer'Size - 1, which is much smaller than System.Max_Binary_Modulus which is based on the size of a 64 bit integer. More below.... > ... >> If we had that, then we could write instead; >> >> pragma Assert((T'Last nand T'Last) = 0); > > Tricky! We probably want the assertion to be understandable to the > relatively causal reader, and this is not that. (Otherwise, we'd have > to repeat it in English so people know what they're allowed to do, > which defeats the point.) I think either assertion is likely to cause some head-scratching for the casual reader (or even a causal reader ;-) ). I think a better solution is to define a boolean expression function whose name describes the property, then the body of the expression function can be more esoteric, tricky, or super-complicated, as it seems we need to do in current Ada. The name of the function documents the intent. e.g generic type Atomic_Type is mod <> with Atomic; package Atomic_Operations.Bitwise with Pure, Nonblocking is function Atomic_Type_Has_Binary_Modulus return Boolean is ((T'Last nand T'Last) = 0) pragma Assert (Atomic_Type_Has_Binary_Modulus); Note, to have the Assert call a function of the package, it needs to be an expression function, otherwise you get a Program_Error due to elaboration problems. So suppose we wanted to write this assertion using current Ada, without adding a nand keyword to the language. This ended up being a real struggle for me, but this is what I ended up with, that seems to work. This seems to handle any modular type, as well as any combination of 'Size aspect applied to the type. (I think, although there may be some cases that dont work. The ones I tried seem to work at least). generic type Atomic_Type is mod <> with Atomic; package Atomic_Operations.Bitwise with Pure, Nonblocking is function Atomic_Type_Has_Binary_Modulus return Boolean is (Atomic_Type'Mod (2) = 0 or else (for all I in 1 .. Atomic_Type'Size - 1 => (for some K in 1 .. I - 1 => 2 * Atomic_Type (2**(K - 1)) < Atomic_Type (2**(K - 1))) or else (Atomic_Type'Last and 2 * Atomic_Type (2**(I - 1))) = 0 or else (for all J in 0 .. I - 1 => (Atomic_Type'Last and Atomic_Type (2**J)) /= 0))); pragma Assert (Atomic_Type_Has_Binary_Modulus); ... I gave up on trying to use 'Modulus. Randy's suggestion worked for non-generic code, but when you try to use this attributes in a generic, I found it too hard to compare the attribute result to test for overflow. This is because 'Modulus result is a universal integer, which is non-static in the generic specification, so you cant compare it to System.Max_Binary_Modulus. Similarly, the argument for the 'Mod attribute is a universal integer, so you have to be careful to not pass in a value that is too large. I also ran into trouble using the expression 2**I, because that the type of I is natural, and so 2**I is an integer expression, which can overflow. So I had to write 2**(I-1), then convert that to the atomic type, and then multiply by 2 to get the modular value that I really wanted to work with. That multiplication by 2 is a modular operation (that can wrap around) The approach is to keep testing higher bits, and if a 1 is found, then check all lower bits to see if there are any zeroes. If a zero bit is found, just ignore it and keep searching. The way I dealt with overflow is handled in the first part of the expression function, where I test all previous iterations to see if the modular type wrapped around. If a wrap around was found then we know we've already got the answer, and just let the remaining iterations finish without checking the else clauses. I must admit, this is a pretty complicated function to just check a modular type to see if the modulus is a power two! There may be a simpler solution, but every idea I came up with kept hitting roadblocks. It would sure be nice to have some sort of nand capability or similar, to make writing such contracts simpler and easier to write. If not for Ada202x, then hopefully a next one after that. But at least it seems there is a way to do it in current Ada, but its not pretty. Alternatively, we could do away with the assertion, and just document that an instance of the generic will raise an exception if the Modular formal type has a modulus that is not a power of two. But it seems that in Ada 202x, one ought to have visible contracts for such an assertion. ****************************************************************

Questions? Ask the ACAA Technical Agent