Groups | Search | Server Info | Keyboard shortcuts | Login | Register [http] [https] [nntp] [nntps]

Groups > comp.compilers > #3354 > unrolled thread

Re: Are there different programming languages that are compiled to the same intermediate language?

Back to article view | Back to comp.compilers

Contents

  Re: Are there different programming languages that are compiled to the same intermediate language? Martin Ward <mwardgkc@gmail.com> - 2023-01-31 14:04 +0000
    Re: Are there different programming languages that are compiled to the same intermediate language? arnold@freefriends.org (Aharon Robbins) - 2023-02-01 08:07 +0000
      Re: Software proofs, was Are there different programming languages that are compiled to the same intermediate language? Spiros Bousbouras <spibou@gmail.com> - 2023-02-05 15:14 +0000
        Re: C arithmetic, was Software proofs, was Are there different Keith Thompson <Keith.S.Thompson+u@gmail.com> - 2023-02-05 16:14 -0800
          Re: C arithmetic, was Software proofs, was Are there different gah4 <gah4@u.washington.edu> - 2023-02-06 13:26 -0800
            Re: C arithmetic, was Software proofs, was Are there different Hans-Peter Diettrich <DrDiettrich1@netscape.net> - 2023-02-07 14:31 +0100
              Re: C arithmetic, was Software proofs, was Are there different gah4 <gah4@u.washington.edu> - 2023-02-08 01:10 -0800
                Re: C arithmetic, was Software proofs, was Are there different gah4 <gah4@u.washington.edu> - 2023-02-09 00:26 -0800
                  Re: C arithmetic, was Software proofs, was Are there different gah4 <gah4@u.washington.edu> - 2023-02-11 00:01 -0800
                    Re: C arithmetic, was Software proofs, was Are there different drb@ihatespam.msu.edu (Dennis Boone) - 2023-02-12 04:37 +0000
              Re: C arithmetic, was Software proofs, was Are there different anton@mips.complang.tuwien.ac.at (Anton Ertl) - 2023-02-08 10:19 +0000
                Re: C arithmetic, was Software proofs, was Are there different Hans-Peter Diettrich <DrDiettrich1@netscape.net> - 2023-02-10 19:11 +0100
                  Re: C arithmetic, was Software proofs, was Are there different gah4 <gah4@u.washington.edu> - 2023-02-10 23:47 -0800
                    Re: C arithmetic, was Software proofs, was Are there different anton@mips.complang.tuwien.ac.at (Anton Ertl) - 2023-02-11 22:34 +0000
                      Re: old floating point, C arithmetic, was Software proofs, was Are there different gah4 <gah4@u.washington.edu> - 2023-02-11 22:48 -0800
              Re: C arithmetic, was Software proofs, was Are there different Hans-Peter Diettrich <DrDiettrich1@netscape.net> - 2023-02-08 15:24 +0100
                Re: C arithmetic, was Software proofs, was Are there different gah4 <gah4@u.washington.edu> - 2023-02-09 00:37 -0800

#3354 — Re: Are there different programming languages that are compiled to the same intermediate language?

On 30/01/2023 10:00, John Levine wrote:
> [Remember that while the halting problem is insoluble in general, it's
> often soluble in specific cases, e.g. "halt" or "foo: goto foo".

More usefully, there are methods for transforming a formal
specification into an executable implementation which
preserve semantic equivalence, and therefore are guaranteed
to produce a terminating program (for input states for which
the specification is defined). For example:

"Provably Correct Derivation of Algorithms Using FermaT"
Martin Ward and Hussein Zedan
Formal Aspects of Computing, September 2014.
Volume 26, Issue 5, Pages 993--1031, 2014-09-01, ISSN: 0934-5043
doi:dx.doi.org/10.1007/s00165-013-0287-2
http://www.gkc.org.uk/martin/papers/trans-prog-t.pdf

> Nevertheless, I would be quite surprised if anyone could prove a
> non-toy translator correct. -John]
According to this paper: "The state of the art [as of 2014] is
the CompCert compiler, which compiles almost all of the C language
to PowerPC, ARM and x86 assembly and has been mechanically verified
using the Coq proof assistant."

Xavier Leroy. "Formally verifying a compiler: Why? How? How far?".
CGO 2011 - 9th Annual IEEE/ACM International Symposium on Code
Generation and Optimization, Apr 2011, Chamonix, France.
⟨10.1109/CGO.2011.5764668⟩. ⟨hal-01091800⟩

https://hal.inria.fr/hal-01091800

--
Martin

Dr Martin Ward | Email: martin@gkc.org.uk | http://www.gkc.org.uk
G.K.Chesterton site: http://www.gkc.org.uk/gkc | Erdos number: 4

[toc] | [next] | [standalone]

#3356

I've never understood this. Isn't there a chicken and egg problem?
How do we know that the theorem prover is correct and bug free?

I ask in all seriousness.

Thanks,

Arnold

In article <23-01-092@comp.compilers>, Martin Ward  <martin@gkc.org.uk> wrote:
>On 30/01/2023 10:00, John Levine wrote:
>> [Remember that while the halting problem is insoluble in general, it's
>> often soluble in specific cases, e.g. "halt" or "foo: goto foo".
>
>More usefully, there are methods for transforming a formal
>specification into an executable implementation which
>preserve semantic equivalence, and therefore are guaranteed
>to produce a terminating program (for input states for which
>the specification is defined).    ...
[It's a perfectly reasonable question. Alan Perlis, who was my thesis
advisor, never saw any reason to believe that a thousand line proof
was any more likely to be bug-free than a thousand line program.
-John]

[toc] | [prev] | [next] | [standalone]

#3365 — Re: Software proofs, was Are there different programming languages that are compiled to the same intermediate language?

On 01 Feb 2023 08:07:24 GMT
arnold@freefriends.org (Aharon Robbins) wrote:
> I've never understood this. Isn't there a chicken and egg problem?
> How do we know that the theorem prover is correct and bug free?

We prove it by hand ? I don't know if anyone has done this for the
provers mentioned but it feels like a feasible task and when it's done ,
it's done i.e. a theorem prover is not the kind of software which
continually gets updated.

> [It's a perfectly reasonable question. Alan Perlis, who was my thesis
> advisor, never saw any reason to believe that a thousand line proof
> was any more likely to be bug-free than a thousand line program.
> -John]

It depends on what we mean by "bug" , in mathematics we wouldn't say "bug"
but "error".

First you have *typos* which is situations where one was meaning to , for
example , write  i  and they  wrote  j  instead. It may be that mathematics
proofs have more of those than computer programmes because in computer
programmes some will be caught by the compiler like for example if  j  has
not been declared. But the essential difference is that a typo is harmless in
mathematics , the reader of the proof will either notice and understand what
was intended or even unconsciously replace what is written with what was
intended. But in computer programmes this kind of typo bug can be
catastrophic. Hence in mathematics we wouldn't say that a proof has errors
just because it has a typo , we would say it has a typo.

For other errors , logic errors , I would guess that computer programmes will
have more errors/bugs than mathematical proofs. This assertion is based on
personal experience and instinct to some extent , having written both many
programmes and many proofs. But I will attempt to give some of what I think
are reasons :

1:
In mathematics you work with a formalism right from the start but in computer
programmes often one has an intuitive understanding of what the program is
meant to achieve and a working programme may be considered to have a bug when
its behaviour turns out not to match closely enough that intuitive
understanding. The difference in the level of formalism is not just about
the programmes but about the programming languages too. In standards of
programming languages I've read , the language is not described in precise
mathematical detail. The grammar usually is but not other parts of the language.

For example , from the C standard :
    The result of the binary + operator is the sum of the operands.

Even just for integer arguments , this is nowhere a complete definition but
to piece together a complete definition one must combine information
scattered in faraway parts of the standard. This would never occur in a
mathematics books or paper , the complete definition of a function or
operator or whatever (including the precise set for which it is defined)
would appear in one place. This sort of thing where one has to piece
together information from many parts of the document to arrive at a complete
definition , seems to be common in computer language standards and I have
no idea why it happens , I don't think anything about specifying a programming
language forces things to be done like this. But the result is that programmers
will often work with a mix of precise specification and intuitive understanding
of the language they're using.

2:
In mathematics a correct proof *is* the goal but in computer programming some
set of behaviours is the goal and the set of behaviours may not even be the
ultimate goal but the desire to make a profit is. For example

en.wikipedia.org/wiki/Pac-Man :
    Due to an integer overflow, the 256th level loads improperly, rendering
    it impossible to complete.

But this didn't prevent the game from being highly successful. "Donkey Kong"
also had a bug which prevented progress from some point onwards.

What is the goal also influences the kind of people who specialise in computer
programming vs those who write mathematical proofs. My impression is that there
exist computer programmers who are of the "trial and error" type who write some
code which seems to approximate what they have in mind , test it , write some
more code and so forth. Eventually they arrive at something which seems to
match their mental model and they consider themselves done. They wouldn't have
any interest and possibly ability to write a proof of correctness. As a practical
matter , they may be perfectly productive and write code which works for the
desired cases.

3:
There is a kind of bug/error for which there's no mathematical analogue :

From  "Expert C Programming" by Peter van der Linden :

    One release of an ANSI C compiler had an interesting bug. The symbol
    table was accessed by a hash function that computed a likely place from
    which to start a serial search. The computation was copiously commented,
    even describing the book the algorithm came from. Unfortunately, the
    programmer omitted to close the comment! The entire hash initial value
    calculation thus fell inside the continuing comment,


[...]

    The entire calculation of the initial hash value was omitted, so the
    table was always searched serially from the zeroth element! As a result,
    symbol table lookup (a very frequent operation in a compiler) was much
    slower than it should have been. This was never found during testing
    because it only affected the speed of a lookup, not the result. This is
    why some compilers complain if they notice an opening comment in a
    comment string. The error was eventually found in the course of looking
    for a different bug. Inserting the closing comment resulted in an
    immediate compilation speedup of 15%!

[The history of formal description of programming languages is not
encouraging. Back in the 1970s the ANSI PL/I standard was defined in
terms of formal operations on trees, but even so it had bugs/errors.
Also, per your comment on addition, in a lot of cases the practical
definition turns into whatever the underlying machine's instruction
does. Until recently the C standard was deliberately unclear about
whether arithmetic was ones- or twos-complement. -John]

[toc] | [prev] | [next] | [standalone]

#3368 — Re: C arithmetic, was Software proofs, was Are there different

[...]
> [The history of formal description of programming languages is not
> encouraging. Back in the 1970s the ANSI PL/I standard was defined in
> terms of formal operations on trees, but even so it had bugs/errors.
> Also, per your comment on addition, in a lot of cases the practical
> definition turns into whatever the underlying machine's instruction
> does. Until recently the C standard was deliberately unclear about
> whether arithmetic was ones- or twos-complement. -John]

The C standard still doesn't mandate two's-complement.

The 1990 edition of the C standard was vague about integer
representations, though it did impose some requirements.  It required
a "pure binary" representation, and it required, for example,
a value that is within the range of both int and unsigned int to
have the same representation in both.  That excluded some of the
more exotic possibilites.  (It mentioned 2's complement a few times,
but only as an example.)

The 1999 standard explicitly required one of three representations:
sign and magnitude, two's complement, or one's complement.  It also
explicitly permitted padding bits (bits that don't contribute
to the value, and that can either be ignored or create trap
representations).

The 2011 standard corrected the spelling of "ones' complement",
but otherwise didn't change anything significant.  (The 2017 edition
was a minor update.)

The upcoming 2023 standard mandates two's complement.  And it
requires INT_MIN to be exactly -INT_MAX-1; previously INT_MIN could
be equal to -INT_MAX, and -INT_MAX-1 could be a trap representation.
It still permits padding bits and trap representations.

Note that twos's complement *representation* doesn't imply two's
complement *behavior* on overflow.  Signed integer overflow still
has undefined behavior.

--
Keith Thompson (The_Other_Keith) Keith.S.Thompson+u@gmail.com
Working, but not speaking, for XCOM Labs
void Void(void) { Void(); } /* The recursive call of the void */

[toc] | [prev] | [next] | [standalone]

#3369 — Re: C arithmetic, was Software proofs, was Are there different

On Sunday, February 5, 2023 at 6:01:04 PM UTC-8, Keith Thompson wrote:

(snip)

> The upcoming 2023 standard mandates two's complement. And it
> requires INT_MIN to be exactly -INT_MAX-1; previously INT_MIN could
> be equal to -INT_MAX, and -INT_MAX-1 could be a trap representation.
> It still permits padding bits and trap representations.

Too bad for those CDC computers, and Unisys computers.
Last I know of sign-magnitude is the IBM 7090 and 7094.


> Note that twos's complement *representation* doesn't imply two's
> complement *behavior* on overflow. Signed integer overflow still
> has undefined behavior.

Overflow behavior mostly depends on the hardware.

Many computers, such as the IBM S/360 and successors, have a bit that
enables or disables the fixed point overflow exception. (For IBM, it
also applies to decimal overflow.)

For IA32, that is x86, there is the INTO instruction, which is put
after any instruction that could generate overflow, and causes the
interrupt if the overflow bit is set. Compilers would have to generate
that instruction.

It seems, though, that has gone away in x86-64 mode.

I don't know that there is any replacement, other than a conditional
branch based on the overflow flag.

Fortran programmers rely on fixed point overflow, as they have been
doing for 60 years, and don't have unsigned.

(There are two routines in TeX that Knuth suggests replacing with
assembly code. Those do multiply and divide, with 32 bit fixed point
values, 16 bits after the binary point. Pascal has no option for
avoiding the overflow trap, and it takes a lot of Pascal code to do
the multiply and divide!)

[toc] | [prev] | [next] | [standalone]

#3371 — Re: C arithmetic, was Software proofs, was Are there different

On 2/6/23 10:26 PM, gah4 wrote:

> Too bad for those CDC computers, and Unisys computers.
> Last I know of sign-magnitude is the IBM 7090 and 7094.

AFAIK use IEEE-754 floating point numbers still sign-magnitude
representation.
Then the same representation of integral numbers may have advantages in
computations.

DoDi
[I presume the sign-magnitude is to enable the hidden bit trick,
which doesn't apply in unscaled integers. -John]

[toc] | [prev] | [next] | [standalone]

#3373 — Re: C arithmetic, was Software proofs, was Are there different

On Tuesday, February 7, 2023 at 6:30:40 PM UTC-8, Hans-Peter Diettrich wrote:
> On 2/6/23 10:26 PM, gah4 wrote:

> > Too bad for those CDC computers, and Unisys computers.
> > Last I know of sign-magnitude is the IBM 7090 and 7094.

> AFAIK use IEEE-754 floating point numbers still sign-magnitude
> representation.
> Then the same representation of integral numbers may have advantages in
> computations.

> [I presume the sign-magnitude is to enable the hidden bit trick,
> which doesn't apply in unscaled integers. -John]

Yes, I meant integer representation.

Well, I have been wondering for years when we get a C compiler
for the 7090 so we can test out sign-magnitude integers.

I think the 7090 does 16 bit integers, at least that is what
its Fortran compilers did, stored in 36 bit words.

As for floating point, the PDP-10 uses a two's complement
floating point format.  It does two's complement on the
whole 36 bit word.  The result is that fixed point compare
instructions work on floating point values.
[The 704x/709x series did 36 bit sign-magnitude arithmetic.  Fortran
integers were limited to 15 bits plus a sign, probably because that
was the size of addresses, and they expected integer arithmetic to
be used only for counting and subscripts.  In 709 Fortran II they
expanded them to 17 bits, in 7090 Fortran IV they were finally a
full word. -John]

[toc] | [prev] | [next] | [standalone]

#3376 — Re: C arithmetic, was Software proofs, was Are there different

On Wednesday, February 8, 2023 at 8:48:23 AM UTC-8, gah4 wrote:

(snip)

> Well, I have been wondering for years when we get a C compiler
> for the 7090 so we can test out sign-magnitude integers.

> I think the 7090 does 16 bit integers, at least that is what
> its Fortran compilers did, stored in 36 bit words.

 (snip)

> [The 704x/709x series did 36 bit sign-magnitude arithmetic. Fortran
> integers were limited to 15 bits plus a sign, probably because that
> was the size of addresses, and they expected integer arithmetic to
> be used only for counting and subscripts. In 709 Fortran II they
> expanded them to 17 bits, in 7090 Fortran IV they were finally a
> full word. -John]

OK, so 7090 C can use all 36 bits.  When we get one.

I just remembered that the S/360 emulation to develop
OS/360 was done on the 7090.  36 bits would help!

It was the 15 bit integers on the 704 that gave us five digit
statement numbers in Fortran, originally 1 to 32767, and
(not much) later extended to 99999.

And over 60 years later, we still have 99999.

But also, the 704 Fortran, and I believe still the 7090,
indexes arrays from the end of memory toward the beginning.
[It did because for reasons I have never been able to figure out,
the 70x series subtracted rather than added the contents of
an index register to get the effective address. -John]

[toc] | [prev] | [next] | [standalone]

#3380 — Re: C arithmetic, was Software proofs, was Are there different

(snip, I wrote)

> But also, the 704 Fortran, and I believe still the 7090,
> indexes arrays from the end of memory toward the beginning.

And or moderator wrote:
> [It did because for reasons I have never been able to figure out,
> the 70x series subtracted rather than added the contents of
> an index register to get the effective address. -John]

I suppose so, but it was also convenient. Compilers (or linkers)
generate code starting from the bottom of memory, and allocate
variables starting from the top. (Different for different sized
machines.) Since Fortran COMMON can be different length, or at least
blank COMMON in later versions, allocating it from the end of memory
works well.

You can extend common from one subroutine to the next, or with
chaining, to another whole program.

So, was Fortran designed around the hardware,
to allocate memory from the end?

Or maybe just lucky.
[Fortran was definitely designed around the 704. I have done a lot of
looking to try and find out where the subtracted index registers came
from, and while there are a lot of guesses, there is nothing written
down. The three index registers were 1,2, and 4, and if you specified
more than one, it OR'ed them together and subtracted the result, which
was really strange. There were a lot of other machines with index
registers but none I know of that subtracted or OR'ed. I have also
been unable to tell whether the OR'ing was deliberate or just a result
of minimizing the number of tubes that they then documented.  It was
likely useless since the 7094 had 7 index registers and a flag in
case you wanted the old behavior. -John]

[toc] | [prev] | [next] | [standalone]

#3382 — Re: C arithmetic, was Software proofs, was Are there different

 > The three index registers were 1,2, and 4, and if you specified more
 > than one, it OR'ed them together and subtracted the result, which was
 > really strange.  There were a lot of other machines with index registers
 > but none I know of that subtracted or OR'ed.  I have also been unable to
 > tell whether the OR'ing was deliberate or just a result of minimizing
 > the number of tubes that they then documented.

Not having to have the circuitry to make sure multiple registers
were never gated onto the internal bus seems like a likely reason.

But one _could_ also conceivably use multiple index registers for
multiple dimensions, with careful allocation.

De
[As I said, I've found lots of guesses but no documents. Multiple
dimensions only work if each dimension is a power of two which,
considering the 704's tiny memory, seems unlikely. My guess is the
same as yours, fewer tubes, but it's just a guess. -John]

[toc] | [prev] | [next] | [standalone]

#3374 — Re: C arithmetic, was Software proofs, was Are there different

Hans-Peter Diettrich <DrDiettrich1@netscape.net> writes:
>AFAIK use IEEE-754 floating point numbers still sign-magnitude
>representation.
>Then the same representation of integral numbers may have advantages in
>computations.

Such as?  Anyway, whatever these advantages may be, they have not been
enough to prevent the extermination of sign-magnitude integers.

>[I presume the sign-magnitude is to enable the hidden bit trick,
>which doesn't apply in unscaled integers. -John]

With a ones-complement or two's-complement mantissa the hidden bit
would just have the same sign as the sign bit, so this trick is not
tied to sign-magnitude representation.

Some years ago someone sketched a two's-complement representation for
FP (that also includes the exponent), but I did not quite get the
details.  Anyway, I expect that whatever the advantages of that
representation are, they are not enough to justify the transition
cost.

- anton
--
M. Anton Ertl
anton@mips.complang.tuwien.ac.at
http://www.complang.tuwien.ac.at/anton/
[PDP-6/10 floating point was two's complement.  As someone else recently noted, that
meant they could use fixed point compare instructions. -John]

[toc] | [prev] | [next] | [standalone]

#3378 — Re: C arithmetic, was Software proofs, was Are there different

On 2/8/23 11:19 AM, Anton Ertl wrote:
> With a ones-complement or two's-complement mantissa the hidden bit
> would just have the same sign as the sign bit, so this trick is not
> tied to sign-magnitude representation.

Please explain the provenience or purpose of that hidden bit with
integral numbers. How can integral values be *normalized* so that a
previously required bit can be hidden? Sign extension to a higher number
of bits does not increase the value or accuracy of an integral number.

DoDi
[He said "mantissa", so it's floating point.  I've certainly seen scaled
integer arithmetic, but normalized integers other than +/- zero in systems
with signed zeros seems unlikely. -John]

[toc] | [prev] | [next] | [standalone]

#3379 — Re: C arithmetic, was Software proofs, was Are there different

On Friday, February 10, 2023 at 10:18:49 AM UTC-8, Hans-Peter Diettrich wrote:

(snip)

> Please explain the provenience or purpose of that hidden bit with
> integral numbers. How can integral values be *normalized* so that a
> previously required bit can be hidden? Sign extension to a higher number
> of bits does not increase the value or accuracy of an integral number.

> [He said "mantissa", so it's floating point. I've certainly seen scaled
> integer arithmetic, but normalized integers other than +/- zero in systems
> with signed zeros seems unlikely. -John]

Normalized binary floating point, with hidden one, is pretty common.
I knew IBM S/360 floating point for some years before learning about
those, and it seemed surprising at the time.

As for integers, though, there are some processors with a floating
point format that does not left normalize values.

Some CDC processors, if the value can be shifted, normalized,
as an integer value without losing bits on either end, choose that.
Even more, the exponent is zero for that case.  I think some
Burroughs processors also do that.

The result of doing that is that, for values in the appropriate range,
the floating point instructions work for integer values. No instructions
are needed to convert (in range) integers to floating point.

There is so much fun history to the different floating point
formats used over the years.  Now almost forgotten.
[I am not aware of any hidden bit formats before IEEE but the 704
manual noted that normalized mantissas always have a 1 in the high
bit so it wasn't a big leap. -John]

[toc] | [prev] | [next] | [standalone]

#3381 — Re: C arithmetic, was Software proofs, was Are there different

gah4 <gah4@u.washington.edu> writes:
>[I am not aware of any hidden bit formats before IEEE

The VAX FP formats have a hidden bit
<https://nssdc.gsfc.nasa.gov/nssdc/formats/VAXFloatingPoint.htm>, and
AFAIK VAX F and G are pretty close to IEEE binary32 and binary64.

According to
<https://home.kpn.nl/jhm.bonten/computers/bitsandbytes/wordsizes/hidbit.htm>
already Zuse used a hidden bit in FP numbers on his machines (1940s
and 1950s).

--
M. Anton Ertl
anton@mips.complang.tuwien.ac.at
http://www.complang.tuwien.ac.at/anton/
[Oh, right, I forgot about Zuse.  He invented a lot of stuff that other
people reinvented later. Squinting at my VAX architecture handbook, the
formats have the same layout as IEEE but the exponents are excess 128 and
1024 rather than 127 and 1023 and there's no infinities or denormals. -John]

[toc] | [prev] | [next] | [standalone]

#3383 — Re: old floating point, C arithmetic, was Software proofs, was Are there different

(our moderator wrote)

> [Oh, right, I forgot about Zuse. He invented a lot of stuff that other
> people reinvented later. Squinting at my VAX architecture handbook, the
> formats have the same layout as IEEE but the exponents are excess 128 and
> 1024 rather than 127 and 1023 and there's no infinities or denormals. -John]

I always forget the difference between them.

VAX has the binary point to the left of the hidden one, and IEEE to the right.
So that makes up for the one difference in exponent bias.

But no infinity and NaN means that the actual exponent can be one higher.

I think that is the way it works.

I never had problems reading S/360 format from hex dumps, where
the exponent is in whole hexdecimal digits, and no hidden one.

[toc] | [prev] | [next] | [standalone]

#3375 — Re: C arithmetic, was Software proofs, was Are there different

On 2/7/23 2:31 PM, Hans-Peter Diettrich wrote:
> On 2/6/23 10:26 PM, gah4 wrote:
>
>> Too bad for those CDC computers, and Unisys computers.
>> Last I know of sign-magnitude is the IBM 7090 and 7094.
>
> AFAIK use IEEE-754 floating point numbers still sign-magnitude
> representation.
> Then the same representation of integral numbers may have advantages in
> computations.
>
> DoDi
> [I presume the sign-magnitude is to enable the hidden bit trick,
> which doesn't apply in unscaled integers. -John]

That's correct, the inprecise representation of FP numbers allows for
such tricks. The hidden bit trick can be used again with the FP
exponents, as I outlined in my Dynamic Floating Point Exponents proposal
<https://figshare.com/articles/preprint/Dynamic_Exponents_for_Floating_Point_Numbers-2022-04-07_pdf/19548187>.

DoDi

[toc] | [prev] | [next] | [standalone]

#3377 — Re: C arithmetic, was Software proofs, was Are there different

On Wednesday, February 8, 2023 at 8:50:19 AM UTC-8, Hans-Peter Diettrich wrote:

(snip)

> That's correct, the inprecise representation of FP numbers allows for
> such tricks. The hidden bit trick can be used again with the FP
> exponents, as I outlined in my Dynamic Floating Point Exponents proposal

To continue discussion about OoO and the 360/91, S/360 specifies
floating point divide with a truncated quotient.   The 91 uses a
Newton-Raphson divide algorithm, using its high-speed multiplier,
to generate a rounded quotient.

Along with imprecise interrupts, that is on the list of incompatibilities
with other S/360 models.

As for hidden bit, S/360 uses base 16 floating point, so no hidden bit.
[I actually programmed a /91 in Fortran, so, yeah. -John]

[toc] | [prev] | [standalone]

Back to top | Article view | comp.compilers

csiph-web