Version 1.1 of ai12s/ai12-0253-1.txt

Unformatted version of ai12s/ai12-0253-1.txt version 1.1
Other versions for file ai12s/ai12-0253-1.txt

!standard A.5.4(0)          18-01-26 AI12-0253-1/01
!class Amendment 18-01-26
!status work item 18-01-26
!status received 18-01-15
!priority Very_Low
!difficulty Medium
!subject Saturation arithmetic for scalar types
!summary
Add three (?) generic packages for saturation arithmetic.
!problem
Saturation arithmetic is commonly used in some fields, including graphical applications and real-time control systems. Ada doesn't provide any way to get saturation arithmetic, although the other features of the language are well-suited to these kinds of applications.
!proposal
(See Summary.)
!wording
** TBD.
!discussion
There seem to be three ways to provide this capability:
(1) With a new kind of type declaration (and associated generic formal types). This would be much like modular types, with all of the advantages and disadvantages of that approach.
(2) With an aspect to modify the behavior of otherwise normal types. This is a problem for generic matching (either way), as writing correct algorithms using saturation math is harder than using normal math (experience with generic modular types shows a similar effect). In addition, the rules for Ada math allow getting the correct answer or overflowing in overflow situations (allowing extra precision) -- that would have to be abandoned for saturated integers even though they use the same set of operations. Also, static expressions would have issues with saturation math similar to that of modular types; changing values of static expressions based on an aspect is unpleasant.
(3) A set of saturation math packages. With the addition of literals for private types, these probably would be just as easy to use as a regular type declaration. Moreover, since these would be generic (taking a saturation value as a formal parameter), they could be used as signatures in a generic unit, thus acting like a formal saturation type parameter. The downside is that these would make it harder to use specialized hardware; but as built-in packages are typical in Ada compilers, it seems possible to do that to target special hardware (on a DSP, for instance). Another downside is that ranges would not easily be available (although predicates could be used to get a similar effect).
The author suggests using packages for this math.
The packages would be generic with a saturation value as a generic parameter. (The fixed and float packages would also pass in a "usual" fixed/float type with the appropriate precision.)
!ASIS
[Not sure. It seems like some new capabilities might be needed, but I didn't check - Editor.]
!ACATS test
ACATS B- and C-Tests are needed to check that the new capabilities are supported.
!appendix

!topic Saturation aspect for scalar types
!reference Ada 2012 RM3.5(10)
!from Gustavo A. Hoffmann 18-01-15
!keywords saturating arithmetic, scalar types
!discussion

This is a proposal for a new Ada aspect for scalar data types that
provides automatic saturation for all operations. This feature would:

    - eliminate the need to override operations;
    - allow for the compiler to create optimal code for the target processor;
       - In case of digital signal processors (e.g. TI C64x platform),
         the compiler could use saturating instructions available for these
         processors.
       - The same applies to MMX instructions for x86-family processors.
    - eliminate a whole class of errors: overflows are not possible;
       - Formal proof of numerical algorithms could be simplified.
    - simplify use of generics: no need to provide the custom saturating
      operations.

The syntax for this new aspect could be as following:

type T is <type_definition> with Saturation => <boolean_expression>

This is an example for fixed-point types:

procedure Test is
    Fract_Depth : constant Positive := 32;
    Fract_Delta : constant := 1.0 / 2.0 ** (Fract_Depth - 1);

    type Sat_Fract is delta
      Fract_Delta range -1.0 .. 1.0 - Fract_Delta
      with Size => Fract_Depth, Saturation => True;

    A, B : Sat_Fract;
begin
    A := 0.75;
    B := 0.75;

    A := A + B;
    --  Result: A = 0.999999...
end Test;

The same strategy could be applied to floating-point data types:

procedure Test is
    type Sat_Fract is new Float range -1.0 .. 1.0
      with Saturation => True;

    A, B : Sat_Fract;
begin
    A := 0.75;
    B := 0.75;

    A := A + B;
    --  Result: A = 1.0
end Test;

Also, the aspect could be used for creating distinct implementations in
special cases. This is a very simple example just to illustrate this case:

generic
    type T is delta <>;
procedure Test is
    A, B : T;
begin
    if T'Saturation then
       A := A + B;
    else
       --  Scaling down A and B to get headroom
       A := (A / 2) + (B / 2);
       --  Scaling up later...
    end if;
end Test;

Although the examples above use fixed-point and floating-point types,
the same approach can be used for integer types. This can be useful for
image processing, for example.

Saturation could also be applied to enumerations. In this case, however,
I don't have an example where this feature could be useful.

****************************************************************

From: Randy Brukardt
Sent: Friday, January 19, 2018  9:28 PM

> This is a proposal for a new Ada aspect for scalar data types that
> provides automatic saturation for all operations. This feature would:
>
>(1)     - eliminate the need to override operations;
>(2)     - allow for the compiler to create optimal code for the target
>          processor;
>        - In case of digital signal processors (e.g. TI C64x
>           platform), the compiler could use saturating instructions available
>           for these processors.
>        - The same applies to MMX instructions for x86-family
>           processors.
>(3)     - eliminate a whole class of errors: overflows are not possible;
>        - Formal proof of numerical algorithms could be simplified.
>(4)     - simplify use of generics: no need to provide the custom
>           saturating operations.
>
> The syntax for this new aspect could be as following:
>
> type T is <type_definition> with Saturation => <boolean_expression>

The following is my personal opinions rather than in my role as ARG Editor.

I numbered the supposed advantages of this proposal so I can refer to them by
number below.

The first problem with this proposal is that the saturation value is not
specified. That matters a lot for evaluating the supposed advantages listed
above.

For instance, consider the declarations:

    type Something is range 0 .. 10000
        with Saturation;

    Obj1 : Something := 102;
    Obj2 : Something'Base := Obj1 * Obj1;

What is the result value for Obj2? There are two possibilities: 10000 (if
Saturation is to Something'Last) or 10404 (if Saturation is to
Something'Base'Last). Note that if the result is the second, then

    Obj3 : Something := Obj2;

raises Constraint_Error. Moreover, the behavior in this case is
implementation-defined and not portable, since the size of the base type is
chosen by the compiler, and can be different for other compilers (even on the
same target).

And if it is the first, then no hardware instructions could possibility be used
to implement it. Advantage (2) is only possibly in very limited circumstances
(essentially if the bounds equals those of the implementation-defined type).

Good Ada code always uses a range based on the requirements of the application
in type declarations, and not some values that happen to force some single
implementation to use some particular type representation.

The ubiquity of bounds checks and other rules means that (3) is simply not true.
First of all, the Ada numeric evaluation model only requires the result to
either be the correct result or Constraint_Error to be raised for overflow.
Overflow is never required, and Ada compilers are allowed to use extra range if
it is available. Moreover, static expressions are evaluated exactly using
infinite range and precision. Saturation math does not fit well into this model,
as it requires every intermediate result to be checked for saturation -- extra
range cannot be allowed. And if an expression is changed slightly so it moves
from a static expression to a dynamic one (or back), the result could vary
wildly.

The allowance of extra range in intermediate results means that it is impossible
to separate bounds and overflow checks in Ada (there is a reason that both raise
the same exception -- that wasn't originally the case). For an expression that
overflows, two things can happen with the same effect -- if the value is
evaluated with extra range (thus it is too large), then a bounds failure will
happen; if the value is evaluated without extra range, an overflow check will
happen instead.

Thus, overflow checks are just a subset of bounds checks. Therefore, the only
time one eliminates "a whole class of errors" with saturation math is if there
are no bounds associated with those values (already noted as bad Ada practice).
Otherwise, you still need to deal with bounds failures (possibly using tools
like CodePeer or SPARK), and the effort is identical either way.

Overflow and bounds checks exist so that a program is not reporting garbage
answers; rather the failure of the algorithm is reported. (This does, of course,
add a requirement to handle such failures.) I tried to think of places where the
failure of the algorithm does NOT need to be known. The only thing I could come
up with is debugging/logging code. But in such quick and dirty code, it's
unlikely that you'd be declaring types anyway, so I don't think that there is
any help here.

I considered the use of saturating math in non-critical statistics gathering. On
the surface, it would be nice to avoid the possibility of overflow in the spam
filter in the statistics. But the problem is that an saturating statistics value
would be hidden as the results are derived from the value. For instance, the
mean is likely to be reported, but that is calculated from Sum and Count
variables. If either of those saturated, the reported mean would be garbage, but
the value would not make this obvious as it is a formula rather than any
specific bound (and that is assuming that the saturated value is easily
recognizable in the first place). One still would have to detect this problem
and prevent the reporting of any saturated values -- but if you are going to do
that, you can also program so that values don't overflow.

I doubt that it would help formal proof (also (3)) any, either, as many of the
identities that we expect for numerics don't hold for saturating math. (They do
for overflowing math, assuming any overflows terminate the calculation as they
do in Ada). For instance, if (A + 1) = B, you don't know if A = B - 1 [A might
equal B if B is the saturating value]. To deal with this, a prover would have to
prove that B is not the saturating value, which is suspiciously similar to
proving the absence of overflow.

Overriding operations is the basis of the Ada model for OOP and ADTs. So (1)
essentially boils down to not wanting to program in Ada. It probably would have
been better stated that "I don't have to program my own saturating math", which
is only an advantage if one already believes saturating math is useful.

(4) is a bit dubious. One can use signature packages or derived types to avoid
importing long lists of operations. On the other hand, allowing saturating and
overflowing math in the same generic (depending on the actual type) complicates
analysis of the code in the generic body (since math operations don't do the
same thing).

It also would prevent universal code sharing for generics, as every operation
for a formal type would have to be thunked. In current Ada, the operations on
most of the formal numeric types operate the same way regardless of what the
actual type is, and the allowance for extra range and precision in intermediate
results means that such a generic can use regular machine code to implement
operations like "+" and "*". However, saturating math would change this
completely, as the code needed implement "+" would be wildly different (much
like it is between integer and modular types). Every operation would have to be
implemented with a dedicated function call, which would be many times slower
than raw code.

This personally would require me to abandon my Ada compiler (which does use such
generic sharing), and probably the Ada business altogether.

Anyway, saturating math seems to me to be mainly a hack to avoid the worst
problems that come from not having a language that checks overflow and bounds.
It's not necessary when you have such a language, and when proof tools already
exist that can prove exception absence in Ada code (SPARK). And it doesn't help
if you do actually care about the results of an calculation, as you still have
to somehow detect the saturation and ensure the reported results are not
considered definitive.

It does have some value for debugging code and probably a few other algorithms,
so it might make sense to have a set of saturating math packages for Ada. Such a
package could be instantiated with the desired saturation value, and being a
generic package, instances of it could be passed to a generic so only a single
generic (package) parameter would be needed. Such a package would be much less
disruptive to the Ada language and its implementation, and (assuming that
various Ada 2020 enhancements come to pass), it wouldn't be any harder to use
than a regular type declaration. (This is the approach that we are planning for
BigNums, and a saturation package could follow a similar design.)

****************************************************************

From: Jeffrey R. Carter
Sent: Saturday, January 20, 2018  4:40 AM

>> (2)     - allow for the compiler to create optimal code for the target processor;
>>        - In case of digital signal processors (e.g. TI C64x
>>          platform), the compiler could use saturating instructions available
>>          for these processors.
>>        - The same applies to MMX instructions for x86-family
>>          processors.
>
> Advantage (2) is only possibly in very limited circumstances
> (essentially if the bounds equals those of the implementation-defined
> type).

As Robert Dewar used to say, if you need specific machine instructions, use a
machine-code insertion.

AIUI, the set of possible implementation-defined types is given by the Integer_n
and Unsigned_n types in package Interfaces. Possibly it would make sense to
define saturating operations for these types. Such operations would not be named
"+", "-", ..., however.

****************************************************************

From: Tucker Taft
Sent: Saturday, January 20, 2018  10:46 AM

Randy, I think you might underestimate the importance of saturation semantics in
real-time control systems, and in graphics.  This is not a question of masking
errors.  This is the way many of these systems are supposed to work, namely that
they saturate at some particular max and/or min value, rather than either
wrapping around or giving some kind of exception.  When we designed a language
and built a custom compiler for an auto company many years ago, saturation
arithmetic was extremely important to them -- in the context of control-system
algorithms for engine control, braking systems, etc.

I have not looked at the proposal in specific, but I am sympathetic toward the
underlying goal.

****************************************************************

From: Randy Brukardt
Sent: Saturday, January 20, 2018  7:13 PM

> Randy, I think you might underestimate the importance of saturation
> semantics in real-time control systems, and in graphics.  This is not
> a question of masking errors.  This is the way many of these systems
> are supposed to work, namely that they saturate at some particular max
> and/or min value, rather than either wrapping around or giving some
> kind of exception.

But the way you write it here, you make it sound circular -- the values saturate
rather than present an error; it's not an error because it saturates. I
postulate that a lot of these algorithms are written this way to avoid handling
errors rather than being a fundamental property. That said, I didn't mean to
imply that there are no such systems (image processing is an obvious example).
But whether there are really enough for the disruption.

> When we designed a language and built a custom compiler for an auto
> company many years ago, saturation arithmetic was extremely important
> to them -- in the context of control-system algorithms for engine
> control, braking systems, etc.
>
> I have not looked at the proposal in specific, but I am sympathetic
> toward the underlying goal.

I'm certainly not against supporting more functionality that is widely used
(even if it shouldn't be), but I don't think one can change the basic principles
of Ada expression evaluation for any purpose -- the effect is just too
widespread. And to support saturation types directly (in ANY way) requires
abandoning the principle that "correct" evaluation is always allowed (rather
than overflow). Not to mention that saturation math isn't even associative! That
would wreak havoc on optimizers and probably require enhancing backends to
specialized support.

I suggested a package a-la Bignum to provide support without forcing compilers
into pervasive changes.

****************************************************************

From: Gautier de Montmollin
Sent: Sunday, January 21, 2018  7:03 AM

> But the way you write it here, you make it sound circular -- the values
> saturate rather than present an error; it's not an error because it
> saturates.

A similar argument could be given for modular types.
However, they are in the Ada standard since the 95 version, although they are
doing terrible things - even worse than saturation arithmetics, like turning
negative numbers into positive ones...

Perhaps you are looking with Ada 83 glasses ?...

****************************************************************

From: Jean-Pierre Rosen
Sent: Sunday, January 21, 2018  12:00 PM

> A similar argument could be given for modular types.

Modular types are different: they correspond to hardware types, and are needed
for interfacing with other languages. This is not true of saturating types.

It has always been the intent that if you need your own arithmetic, you write it
yourself. What's bad with having a package for saturating types?

****************************************************************

From: Randy Brukardt
Sent: Monday, January 22, 2018  3:22 PM

>A similar argument could be given for modular types.
>However, they are in the Ada standard since the 95 version, although
>they are doing terrible things - even worse than saturation
>arithmetics, like turning negative numbers into positive ones...

Yes of course. There is no justification for Ada 95 modular types, they are far
more evil than saturation math. I have always complained that it is impossible
to write safe (overflow checked) code with unsigned representations. Our code
generator can do it, but there isn't any legitimate language way to describe
such a type without having a larger signed representation available.

>Perhaps you are looking with Ada 83 glasses ?...

Just because Ada has one evil datatype does not imply that we should add more
evil datatypes. Two wrongs do not make a right. :-)

****************************************************************

From: Randy Brukardt
Sent: Monday, January 22, 2018  10:09 PM

To expand on this glib answer a bit, Ada 95 recognized that modular math and
integer math are completely different beasts: generic formal signed integer
types and modular types are completely separate -- you cannot use one with the
other. One does not have to try to figure out what will happen with generic
operations that could either wrap around at some unknown modulus or overflow.
(Experience has shown that it is extremely difficult to write correct generics
for modular types -- see the discussion justifying the addition of the Mod
attribute in AI95-0340-1 for an example -- so this is an important decision.)

The (original) proposal here doesn't make that separation; it just blends all of
the kinds of math together and says "now figure out what this code does in
general". If saturation math was kept separate from regular integer/float/fixed
types I would have much less objection. (But of course that makes the proposal
much heavier if the types are built-in.)

****************************************************************

From: Jeff Cousins
Sent: Monday, January 22, 2018  5:41 PM

Modular types always seemed like an dubious compromise to try to satisfy the
many users who really wanted language defined unsigned types, which would then
make use of unsigned arithmetic machine instructions.

****************************************************************

From: Joey Fish
Sent: Tuesday, January 23, 2018  2:43 PM

I rather agree, the problem as I see it is that there are multiple things
mod-types are addressing which are actually discrete; the big ones are:

1. Cyclic nature.
2. Signed/unsigned representation.
3. The "natural base" (excess-K) offset; this is set to zero in modular-types,
   which is, I think, a bad choice as this keeps us from saying, in effect,
   "Type Index is mod 16 with Size => 4;" which would be a type with values
   1..16 with cyclic properties.

****************************************************************

Questions? Ask the ACAA Technical Agent