Ivan Godard <ivan@millcomputing.com> writes:

> On 3/7/2022 11:58 PM, David Brown wrote:
>
>> On 07/03/2022 22:48, MitchAlsup wrote:
>>
>>> On Monday, March 7, 2022 at 2:24:27 PM UTC-6, David Brown wrote:
>>>
>>>> On 07/03/2022 16:02, Ivan Godard wrote:
>>>>
>>>>> On 3/7/2022 12:34 AM, David Brown wrote:
>>>>>
>>>>>> Extra parenthesis makes things abundantly clear at a glance - the reader
>>>>>> can be in no doubt. They are useful for operators that are relatively
>>>>>> rarely used or rarely used in particular combinations, but they are also
>>>>>> useful to give the reader an idea of how you are building up the
>>>>>> expression logically. Maybe "(a + b) + (c + d)" gives the reader more
>>>>>> information than just "a + b + c + d". Making code clear to read - so
>>>>>> that the compiler and the reader are in sync - is vital.
>>>>>
>>>>> Which is why having no precedence at all, just lexical order on the
>>>>> page, gets rid of all the problems.
>>>>
>>>> That would get rid of such problems (though obviously it is not
>>>> applicable to C or C-like languages). However, it would introduce new
>>>> problems - people expect "a + b * c" to have the same precedence as in
>>>> normal mathematics.
>>>
>>> Only when you have never written in a precedence-free language.
>>> a + b * c
>>> Reads just like ASM:
>>> ADD Rt,Ra,Rb
>>> MUL Rt,Rt,Rc
>>
>> I've written plenty of assembly. But assembly is not a precedence-free
>> language - it is a language using prefix functional notation. That is a
>> very different thing.
>>
>> I know there /are/ languages without operator precedence, where
>> "a + b * c" is "(a + b) * c". And I expect that people who use
>> them get used to it. But I think it would take a fair amount of
>> effort for most people to change their thinking when starting
>> with such a language, and mistakes and misunderstandings would be
>> common.
>
> Data point: I have not written APL, but have read quite a bit of
> commentary, and while there were complaints about the symbolic
> notation and the need for quite a bit of math background to grasp
> the effect of some of the operators, I do not recall any
> complaints about absence of precedence.
>
> Data point: there was an operating system and quite a bit of
> embedded code written in Mary1, with no complaints about precedence.
> That may have been because people were thinking of their problem in
> machine terms before coding, instead of mathematical expression
> terms, so they naturally wrote the instructions they wanted in the
> order they wanted them to execute, which was textual order in Mary.
> Multiply is not a common operation in OS code once address
> multiplies are pulled into subscript notation, which Mary did.

Both APL and Mary make other syntactic choices to make those
languages more amenable to right-to-left or left-to-right
ordering. (Disclaimer: what little I know about Mary is from its
wikipedia article; my efforts to locate anything more substantial
have been unsuccessful.) In Mary, for example, assignment happens
on the right, after the expression of the value to be assigned.
It would be hard to make C into a precedence-free and similarly
amenable language without radically revising its expression
syntax.

Also, for APL, it seems quite possible that grappling with the
notation and the unusual math concepts means that people never
got around to complaining about precedence. Footnote: I have
heard from someone who is in a position to know that even Ken
Iverson wrote APL starting at the right and writing towards
the left. What does that say?

Designing a language to work effectively with no precedence rules
other than right-to-left or left-to-right means there will be
tradeoffs in other areas of expression syntax. Although that
might be viable for a new language, I suspect it's unworkable in
any established language such as C or Python or Java, because
their choices in other areas of expression syntax would produce
ungainly results to cope with the altered precedence rules.

MitchAlsup <MitchAlsup@aol.com> writes:

> On Wednesday, March 9, 2022 at 1:50:30 PM UTC-6, Ivan Godard wrote:
>
>> On 3/9/2022 10:00 AM, Anton Ertl wrote:
>>
>>> Ivan Godard <iv...@millcomputing.com> writes:
>>>
>>>> On 3/7/2022 12:19 AM, Anton Ertl wrote:
>>>>
>>>>> I think that type systems are an area where formal descriptions are
>>>>> relatively close to being good enough to being used. The main problem
>>>>> is that every programming language has its own type system with its
>>>>> own twists, that results in its own notation. There is no unifying
>>>>> notation like (E)BNF or stack effect notation that is usable for
>>>>> describing many languages.
>>>>
>>>> There is such: VWG, perhaps others.
>>>
>>> What formal notations I have seen in this area are not close to VWG.
>>>
>>>> There are two problems: VWG itself
>>>> is a mouthful, and to formalize a type system by any complete and
>>>> correct means you have to have defined the system, and no new language
>>>> has gotten all the arm-waving out.
>>>
>>> If we had a successful formal notation, that would be no problem. The
>>> way that the language designer wrote down the formal notation would
>>> settle it; and if there were any problems with the result, they would
>>> be attacked in later revisions; or in prose (like the dangling else is
>>> dealt with in the Pascal Report).
>>>
>>> But we have no successful formal notation for type systems.
>>
>> Depends on what "successful" means :-) If "does the job" then we have
>> some. If "is intellectually tractable in the face of politics" then we
>> don't.
>
> I, personally, have never seen a type system that can even
> annotate all of the exceptions that can be raised on calculations
> of type,

It's easy to define such a type space. The question is, once it has
been defined, what would you do with it?

> or explain why ADD can overflow but AND cannot; or that ADD can
> overflow by 1-bit and multiply can overflow by n-1-bits.

As a rule formal systems never answer "why" questions. The syntax
for C, for example, gives a specification for what programs are
syntactically legal, but says nothing at all about why that
syntax was chosen. It's just a specification, nothing more.

anton@mips.complang.tuwien.ac.at (Anton Ertl) writes:

> Ivan Godard <ivan@millcomputing.com> writes:
>
>> On 3/7/2022 12:19 AM, Anton Ertl wrote:
>>
>>> I think that type systems are an area where formal descriptions are
>>> relatively close to being good enough to being used. The main problem
>>> is that every programming language has its own type system with its
>>> own twists, that results in its own notation. There is no unifying
>>> notation like (E)BNF or stack effect notation that is usable for
>>> describing many languages.

There is a good theoretical reason for that. BNF (and also EBNF)
corresponds to a particular formal model of computation, one
level of the Chomsky hierarchy. There are only four levels in
the Chomsky hierarchy, and the two with more expressive power
than context-free languages are a LOT more expressive. AFAIAA
there is no formal model of computation known between push-down
automata (aka context-free languages) and LBAs (aka linear
bounded automata, aka context-sensitive languages). So if you
want a formal description in a system that has more expressive
power than syntax, which is pretty much a requirement for a type
system, then you're going to end up with something equivalent to
a context-sensitive language (or a general rewrite grammar, which
is Turing equivalent).

In practice people want their type systems to be decidable both
for programs that are type correct and for programs that are not
type correct, and neither CSLs nor GRGs satisfy that property.
So they choose a notational system that is less powerful than
CSLs, but such systems necessarily have less power than might be
desired in another language. Any given formal model is either
potentially not powerful enough or too powerful, so people keep
inventing new ones.

>> There is such: VWG, perhaps others.
>
> What formal notations I have seen in this area are not close to VWG.
>
>> There are two problems: VWG itself
>> is a mouthful, and to formalize a type system by any complete and
>> correct means you have to have defined the system, and no new language
>> has gotten all the arm-waving out.
>
> If we had a successful formal notation, that would be no problem. The
> way that the language designer wrote down the formal notation would
> settle it; and if there were any problems with the result, they would
> be attacked in later revisions; or in prose (like the dangling else is
> dealt with in the Pascal Report).
>
> But we have no successful formal notation for type systems.

The reason why is explained above. As type systems become more
ambitious, there is a need for more expressive power in the
formal model, which ultimately leads to newer formal models that
are more expressive than the existing ones.

MitchAlsup wrote:
> On Wednesday, March 9, 2022 at 11:38:27 AM UTC-6, EricP wrote:
>> MitchAlsup wrote:
>>> On Tuesday, March 8, 2022 at 9:58:52 AM UTC-6, EricP wrote:
>>>> Ivan Godard wrote:
>>>>> On 3/7/2022 11:10 AM, EricP wrote:
>>>>>> Ivan Godard wrote:
>>>>>>> On 3/7/2022 7:10 AM, EricP wrote:
>>>>>>>> - user mode exception/signal handler entry,exit
>>>>>>> Why are exceptions different from calls you didn't ask for?
> <
> Note the word exception here

Yes, and...?

Exceptions are alternate execution paths defined by the ISA
and triggered as side effects of some instructions.
In a sense you did ask for them by, say, dividing by zero.

> <
>>>>>> If I was doing it, the OS deposits (pushes) a packet of exception info
>>>>>> and the return PC onto the apps' user mode stack, and OS returns to
>>>>>> the exception routine. User mode exception handler saves the full integer
>>>>>> context on the stack, and calls the exception dispatcher routine
>>>>>> passing pointers to the exception info and saved context structs as args.
>>>>>> Exception handlers can edit saved context as they wish.
>>>>>> When handlers return, exception dispatcher reloads the now possibly
>>>>>> edited
>>>>>> interrupted context, restores stack, and returns to the possibly
>>>>>> edited PC.
>>>>> How do you do it if there are no modes?
>>>> The main problem is how does exception information get delivered
>>>> to the offending execution, since exceptions are non-maskable so
> <
> Note the word exception here
> <
>>> <
>>> FP-imprecise is maskable on essentially every machine.
>>> <
>>> You just have to have a good plan as to what happens when a masked
>>> exception transpires. Many of them disappear silently (integer overflow
>>> wraps), many of them get different results (FP overflows to infinity) and
>>> some of them result in termination (page fault).
> <
>> Yes. But float exception masking different from interrupt masking.
>> Since it is enabled under user control, the OS has to be prepared
>> to deal with their possibile arrival in any case.
> <
> I was answering the posed point. Interrupts are different from exceptions
> and you specifically used the word exceptions. BTW in my design
> interrupts are not masked, and certainly not masked by a CPU.

The point I'm making is that the difference is in reentrancy
and its control.

>> The problem for exceptions, and why they are different from maskable
>> interrupts, is reentrancy - exception are potentially infinitly reentrant.
>> Since exceptions are defined by the ISA, not triggering one is
>> often just a matter of not doing anything that could cause one.
>>
>> Avoiding reentrancy in the float exception handler is as easy as
>> just not using any float instructions in the non-reentrant portion
>> of the OS handler until the HW exception info block has been saved
>> in a reentrant place, i.e. copy it to the threads' kernel stack.
>>
>> Reentrancy is why I put Errors in a different category from Interrupts
> <
> Can you define the term Error ? Error = "Machine Check" ?

Yes, though I do not mean x86 style machine check which is basically
a whole new mode they slide underneath the existing architecture.

Its any notification of an unusual event that is not delivered by
the ISA defined exceptions or the usual device interrupt mechanism(s).

> <
>> and Exceptions. Like exceptions, errors are usually nonmaskable and
>> potentially infinitely reentrant. Like exceptions, some errors cause
>> instruction abort, others are delivered after instruction finishes.
>> Like interrupts, errors can be synchronous or asynchronous.
> <
> Interrupts are, by definition, asynchronous.
> <
>> Unlike exceptions, some errors cannot be avoided by simply not doing
>> certain things, so you have to deal with the possible reentrancy
>> (e.g. memory errors in the memory error handler routine).
> <
> How is this different from a page fault in the page fault handler ?

Page fault in non pagable memory sections is defined as an OS software bug.
Page fault handlers are stored in non pagable memory sections.
They are, in a sense, blocked by fiat and verified as not occurring.

In VMS and WinNT, and probably Linux and other OS too, page fault is not
allowed in the page fault handler or in many/most parts of the OS.
The first thing thread page fault handlers do is check if a flag is set and
crash if it is. Then they set the flag to block page fault reentrancy.
It also checks the IRQL and if >= DISPATCH it crashes.

Errors cannot be blocked by designing software a certain way.
No arrangement of the OS software can guarentee no memory error in
the memory error handler.

So I take all the nice and easily handled stuff called exceptions and
interrupts and put them in two piles. And I take all the messy stuff,
label it "Here be dragons" and put it in a different pile.

> <
>> Unlike exceptions and interrupts, after errors instructions may
>> or may not be restartable, and this may be model specfic.
>> While exceptions are defined by the ISA, delivery of exception,
>> interrupt and error information is HW model specific.
>>> <
>>>> a single set of registers could be overwritten by multiple exceptions.
>>>>
>>>> Pushing an exception descriptor on the stack is the usual way to handle
>>>> this but that has its own issues, like page faults pushing the packet,
>>>> stack overflow, variable exception packet size complicates interrupt return.
>>>> Also it assumes the ISA has a designated stack register, and may require
>>>> coordination of stack allocation with the OS like Linux "red zones".
>>>>
>>>> If its not hardware pushing the packet then the OS emulates this where
>>>> an exception halts the app thread, spilling its context to memory.
>>>> Then kernel thread edits the app stack and context to push the
>>>> exception packet on the app stack and the PC to a exception handler,
>>>> and then restarts the app thread. This is basically what WinNT does.
>>>>
>>>> The main complaint that people seem to have is that exceptions are
>>>> too expensive, or that the trip through the operating system to
>>> s/trip/excursion/
>>>> deliver them is too expensive.
>>> <
>>> A lot of this is that: it takes hundreds of cycles to get from user mode code
>>> exception to handler mode code, and hundreds of cycles to get back, then
>>> another hundred cycles to get the caches warmed up again.
>>> <
>>> If only there were a way to make those "hundreds" into <say> 10-cycles.
>> I think everyone agrees that x86 has 40 years of barnacles attached
>> to its interrupts and exceptions.
>> And there are multiple ways to not step in the same cow pies.
>>
>> Since I have super and user mode, I would start by pipelining the mode
>> change wherever possible, by attaching the Super/User flag to each uOp.
>> That gets rid of the pipeline drain and bubble for SysCall,
>> Return from Exception or Interrupt REI, and device interrupts.
>> It remains for exceptions as for me they are only recognized at retire.
> <
> Lipstick on a pig......much of the need to drain the pipeline at Syscall is
> because you need pending but unrecognized exceptions to be raised
> in the thread before Syscall transfers control. Blame vonNeumann (i.e.,
> precise exceptions); not me.

Naw, it's a feisty, young, piglet - fast, lean, agile.
With attitude.
And lipstick.

Syscall, REI instructions don't need to drain the pipeline.
As I envision it, Decoder has a future copy the the S/U mode flag
that it copies into each uOp. If there is an exception pending for
a different uOp then when it reaches Retire, the exception triggers
a pipeline drain and restores the S/U mode flag to its prior value.
If a branch mispredict occurs, the checkpoint rollback purges
the following instructions including the Syscall or REI.
However since that almost never occurs, most Syscall and REI
instructions can proceed pipelined like any others.

Interrupts too can be pipelined by a similar mechanism.
When an interrupt request arrives, it redirects Fetch to load the
handler instructions into a fetch buffer, while it continues to
draw instructions for the current stream already in fetch buffer.
When that interrupt fetch buffer is loaded, only THEN does fetch
jam a special Interrupt uOp into the front end and begin pulling
instructions from the handler.
When Decoder sees the Interrupt uOp, it treats it like a Syscall
and switches its future mode flag to Super, which it then attaches
to all subsequent interrupt handler uOps.

On 3/9/2022 1:47 PM, Tim Rentsch wrote:
> Ivan Godard <ivan@millcomputing.com> writes:
>
>> On 3/7/2022 11:58 PM, David Brown wrote:
>>
>>> On 07/03/2022 22:48, MitchAlsup wrote:
>>>
>>>> On Monday, March 7, 2022 at 2:24:27 PM UTC-6, David Brown wrote:
>>>>
>>>>> On 07/03/2022 16:02, Ivan Godard wrote:
>>>>>
>>>>>> On 3/7/2022 12:34 AM, David Brown wrote:
>>>>>>
>>>>>>> Extra parenthesis makes things abundantly clear at a glance - the reader
>>>>>>> can be in no doubt. They are useful for operators that are relatively
>>>>>>> rarely used or rarely used in particular combinations, but they are also
>>>>>>> useful to give the reader an idea of how you are building up the
>>>>>>> expression logically. Maybe "(a + b) + (c + d)" gives the reader more
>>>>>>> information than just "a + b + c + d". Making code clear to read - so
>>>>>>> that the compiler and the reader are in sync - is vital.
>>>>>>
>>>>>> Which is why having no precedence at all, just lexical order on the
>>>>>> page, gets rid of all the problems.
>>>>>
>>>>> That would get rid of such problems (though obviously it is not
>>>>> applicable to C or C-like languages). However, it would introduce new
>>>>> problems - people expect "a + b * c" to have the same precedence as in
>>>>> normal mathematics.
>>>>
>>>> Only when you have never written in a precedence-free language.
>>>> a + b * c
>>>> Reads just like ASM:
>>>> ADD Rt,Ra,Rb
>>>> MUL Rt,Rt,Rc
>>>
>>> I've written plenty of assembly. But assembly is not a precedence-free
>>> language - it is a language using prefix functional notation. That is a
>>> very different thing.
>>>
>>> I know there /are/ languages without operator precedence, where
>>> "a + b * c" is "(a + b) * c". And I expect that people who use
>>> them get used to it. But I think it would take a fair amount of
>>> effort for most people to change their thinking when starting
>>> with such a language, and mistakes and misunderstandings would be
>>> common.
>>
>> Data point: I have not written APL, but have read quite a bit of
>> commentary, and while there were complaints about the symbolic
>> notation and the need for quite a bit of math background to grasp
>> the effect of some of the operators, I do not recall any
>> complaints about absence of precedence.
>>
>> Data point: there was an operating system and quite a bit of
>> embedded code written in Mary1, with no complaints about precedence.
>> That may have been because people were thinking of their problem in
>> machine terms before coding, instead of mathematical expression
>> terms, so they naturally wrote the instructions they wanted in the
>> order they wanted them to execute, which was textual order in Mary.
>> Multiply is not a common operation in OS code once address
>> multiplies are pulled into subscript notation, which Mary did.
>
> Both APL and Mary make other syntactic choices to make those
> languages more amenable to right-to-left or left-to-right
> ordering. (Disclaimer: what little I know about Mary is from its
> wikipedia article; my efforts to locate anything more substantial
> have been unsuccessful.)

https://www.bookdepository.com/Mary-Programming-Language-Norton-Fausto-Garfield/9786136786452

On Wednesday, March 9, 2022 at 6:35:46 PM UTC-6, EricP wrote:
> MitchAlsup wrote:
> > On Wednesday, March 9, 2022 at 11:38:27 AM UTC-6, EricP wrote:
> >> MitchAlsup wrote:
> >>> On Tuesday, March 8, 2022 at 9:58:52 AM UTC-6, EricP wrote:
> >>>> Ivan Godard wrote:
<snip>
> > Lipstick on a pig......much of the need to drain the pipeline at Syscall is
> > because you need pending but unrecognized exceptions to be raised
> > in the thread before Syscall transfers control. Blame vonNeumann (i.e.,
> > precise exceptions); not me.
<
> Naw, it's a feisty, young, piglet - fast, lean, agile.
> With attitude.
> And lipstick.
>
> Syscall, REI instructions don't need to drain the pipeline.
<
I agree, you just have to be able to back out of a syscall ½ way
through if an instruction still in the pipeline raises an exception.
The x86s I worked on did not have the execution window extend
into microcode and had other pipeline anomalies wrt microcode.
<
> As I envision it, Decoder has a future copy the the S/U mode flag
> that it copies into each uOp. If there is an exception pending for
> a different uOp then when it reaches Retire, the exception triggers
> a pipeline drain and restores the S/U mode flag to its prior value.
> If a branch mispredict occurs, the checkpoint rollback purges
> the following instructions including the Syscall or REI.
> However since that almost never occurs, most Syscall and REI
> instructions can proceed pipelined like any others.
<
Right, you just have to drag all state changes through the pipe
and be in a position to undo them.
>
> Interrupts too can be pipelined by a similar mechanism.
> When an interrupt request arrives, it redirects Fetch to load the
> handler instructions into a fetch buffer, while it continues to
> draw instructions for the current stream already in fetch buffer.
> When that interrupt fetch buffer is loaded, only THEN does fetch
> jam a special Interrupt uOp into the front end and begin pulling
> instructions from the handler.
<
Some would complain of interrupt latency; failing to make the
distinction between control arriving, and being to do something
useful.
<
> When Decoder sees the Interrupt uOp, it treats it like a Syscall
> and switches its future mode flag to Super, which it then attaches
> to all subsequent interrupt handler uOps.
<
While you are fetching ISR code, you should also be prefetcing
all of the other control registers needed to run the ISR efficiently.
>
> There are some fiddly bits, rare race conditions like when an
> Interrupt Disable or Enable instruction is in flight in the pipeline.
> Or if a branch mispredict from the prior stream purges the uOp queue
> after it began fetching interrupt stream instructions.
> But nothing unmanageable.
<
You could probably make a rule where you ignore the branch
predictor for the first 100-odd cycles in an ISR:: backwards always
predict taken, forward always predict non-taken.
>
> Taken together with MMU block translate and dedicated SRAM these
> should get 95% of the potential benefits for 10% of the cost.
> >> A small hardware stack eliminates memory accesses to save the
> >> nested interrupted PC and context.
> >> Having exception and interrupt handler addresses calculated eliminates
> >> the memory table lookup, allowing direct immediate handler dispatch.
> > <
> > It is still likely missing its code cache footprint.
> That's what the 4kB SRAM block below takes care of.
> >> An MMU with block address translate eliminates TLB misses for most OS
> >> code and data.
> >>
> >> A small special 4kB block of per-cpu SRAM can store the interrupt
> >> and exception handler prologues and epilogues. Combined with the
> >> MMU block translate allows the fetch buffers to be loaded immediately.
> > <
> > You could always to the PDP-11 trick: if control arrives; the core gets to
> > completely execute 1 instruction before relinquishing. This instruction
> > could be ENTER. Afterwards, you can take another interrupt/exception
> > to the same handler/thread.
> PDP-11 had a Priority Interrupt Controller controlled by 3 bits
> in the Program Status Word to mask equal or lower priority interrupts.
> > <
> >>> <
> >>>> Aside from page fault of valid addresses, which is handled by the OS anyway,
> >>>> the only exception that is performance critical is the recent introduction
> >>>> of hardware transaction memory HTM aborts delivered directly to the app.
> >>> <
> >>> This is why I banned exceptions from ESM ATOMIC events. Exceptions inside
> >>> an ATOMIC event cause control transfer to failure location BEFORE raising
> >>> the exception.
> > <
> >> Yes, I don't want this as an exception either as I don't want to
> >> roll back the register set to the start of the transaction.
> >>
> >> Firstly because from a user point of view they will want to
> >> pass information from inside a failed transaction to outside.
> > <
> > how much more than "it failed" is wanted outside ? everything dealing
> > with intermediate state has become stale.
<
> I'm thinking wanting to know which of multiple memory ops failed?
<
Could have failed because an interrupt arrives {spurious}
<
> Maybe why it failed - was it a write-write collision or read-write?
<
My 66000 has a why register you can sample after a failed event.
<
> One might want to propagate info read during the transaction to the
> failure handler to better tune its response, maybe adjust the backoff.
<
or maybe pick a different item in the queue to remove.
>
> Those who don't like this can do an STM before a transaction and LDM after.
> >> Secondly, from a hardware point of view, the current mechanism for
> >> rolling back register changes is a checkpoint. However a checkpoint
> >> retires when its associated instruction retires. The means that
> >> the a transaction ATXSTART instruction could not retire until
> >> it processed and was ready to retire the ATXCOMMIT instruction.
> >> By not defining a transaction as a register checkpoint, it goes away.
> > <
> > I specifically left a means for code to leave a trail of data that can be
> > <say> printf()ed if the event fails. You can't to this with checkpoint
> > recovery. I agree.
> > <
> >> Or I'd have to figure out a whole different way to manage
> >> checkpoint, rollback, register rename and free lists.
> > <
> > Importantly, in my definition space: ATOMIC stuff is outside of
> > vonNeumann precision. Due to data dependencies, if an event fails
> > an instruction leaving a trail that is programmatically later than
> > another instruction also leaving a trail, the later can have executed
> > while the former did not. When the event fails, control transfers
> > as fast as possible with latent instructions being cancelled.
<
> I trust the users to work out their causality relationships once told
> the rules. I think the rules on current HTM are too constrained.
> And if they bugger it up, it's their program that's broken.

On 3/9/2022 12:12 PM, MitchAlsup wrote:
> On Wednesday, March 9, 2022 at 1:50:30 PM UTC-6, Ivan Godard wrote:
>> On 3/9/2022 10:00 AM, Anton Ertl wrote:
>>> Ivan Godard <iv...@millcomputing.com> writes:
>>>> On 3/7/2022 12:19 AM, Anton Ertl wrote:
>>>>> I think that type systems are an area where formal descriptions are
>>>>> relatively close to being good enough to being used. The main problem
>>>>> is that every programming language has its own type system with its
>>>>> own twists, that results in its own notation. There is no unifying
>>>>> notation like (E)BNF or stack effect notation that is usable for
>>>>> describing many languages.
>>>>>
>>>>> - anton
>>>>
>>>> There is such: VWG, perhaps others.
>>>
>>> What formal notations I have seen in this area are not close to VWG.
>>>
>>>> There are two problems: VWG itself
>>>> is a mouthful, and to formalize a type system by any complete and
>>>> correct means you have to have defined the system, and no new language
>>>> has gotten all the arm-waving out.
>>>
>>> If we had a successful formal notation, that would be no problem. The
>>> way that the language designer wrote down the formal notation would
>>> settle it; and if there were any problems with the result, they would
>>> be attacked in later revisions; or in prose (like the dangling else is
>>> dealt with in the Pascal Report).
>>>
>>> But we have no successful formal notation for type systems.
>> Depends on what "successful" means :-) If "does the job" then we have
>> some. If "is intellectually tractable in the face of politics" then we
>> don't.
> <
> I, personally, have never seen a type system that can even annotate all of the
> exceptions that can be raised on calculations of type, or explain why ADD can
> overflow but AND cannot; or that ADD can overflow by 1-bit and multiply can
> overflow by n-1-bits.

Specifications don't answer"why" questions, they just say what writings
and transformations are legal.

VWG is a rewrite system in which the source text of a program is
repeatedly rewritten according to the rules of the formal specification,
and if the eventual result is empty text then the original program is
syntactically, semantically, and (if the language has a type system)
typeically correct. The specification does not say what it means, for
any value of "means".

According to Tim Rentsch <tr.17687@z991.linuxsc.com>:
>As a rule formal systems never answer "why" questions. The syntax
>for C, for example, gives a specification for what programs are
>syntactically legal, but says nothing at all about why that
>syntax was chosen. It's just a specification, nothing more.

The C standards committee has published separate rationale documents
explaining why they did what they did.

Here's a draft of the C99 rationale:

http://www.open-std.org/jtc1/sc22/wg14/www/docs/n937.pdf

--
Regards,
John Levine, johnl@taugh.com, Primary Perpetrator of "The Internet for Dummies",
Please consider the environment before reading this e-mail. https://jl.ly

> In practice people want their type systems to be decidable both
> for programs that are type correct and for programs that are not
> type correct, ...

I believe this is not the case. Decidability is often used in academic
literature, but it's actually neither necessary nor sufficient:

- It's not sufficient because a decidable type checking algorithm whose
"usual" complexity is too high will not make the cut. In practice
type checking algorithms are expected to be not much worse than O(N)
in the size of the input program, for a "normal program".
- It's not necessary because it's considered acceptable if type checking
does not terminate in some unusual cases (witness C++'s
Turing-complete template system, or any language with procedural
macros).

So the real requirement is one that we don't know how to formalize
mathematically (it's something like "type checking should be fairly fast
for «normal» programs, for some definition of «normal»"), and
"decidable" happens to be the next closest thing we know how to
formalize mathematically.

Stefan

On 10/03/2022 03:07, John Levine wrote:
> According to Tim Rentsch <tr.17687@z991.linuxsc.com>:
>> As a rule formal systems never answer "why" questions. The syntax
>> for C, for example, gives a specification for what programs are
>> syntactically legal, but says nothing at all about why that
>> syntax was chosen. It's just a specification, nothing more.
>
> The C standards committee has published separate rationale documents
> explaining why they did what they did.
>
> Here's a draft of the C99 rationale:
>
> http://www.open-std.org/jtc1/sc22/wg14/www/docs/n937.pdf
>

That is primarily to say why changes were made to the specifications.
It gives answers to some "why" questions, but not many. And it is not
part of the language specifications or standards - if the rationale
differs from the standard (and it does, in some cases, as far as I
remember) then the standard is what matters.

Ivan Godard <ivan@millcomputing.com> writes:

> On 3/9/2022 1:47 PM, Tim Rentsch wrote:
>
>> [...] (Disclaimer: what little I know about Mary is from its
>> wikipedia article; my efforts to locate anything more
>> substantial have been unsuccessful.)
>
> https://www.bookdepository.com/Mary-Programming-Language-Norton-Fausto-Garfield/9786136786452

That page reports "Currently unavailable".

Doing a search at https://www.gettextbooks.com, it reports

No copies of this book were found in stock from
834 online book stores and marketplaces.

It gives the same result looking for "Mary textbook", which
was originally published in the 1970s (fourth edition 1979
IIANM).

John Levine <johnl@taugh.com> writes:

> According to Tim Rentsch <tr.17687@z991.linuxsc.com>:
>
>> As a rule formal systems never answer "why" questions. The syntax
>> for C, for example, gives a specification for what programs are
>> syntactically legal, but says nothing at all about why that
>> syntax was chosen. It's just a specification, nothing more.
>
> The C standards committee has published separate rationale documents
> explaining why they did what they did.
>
> Here's a draft of the C99 rationale:
>
> http://www.open-std.org/jtc1/sc22/wg14/www/docs/n937.pdf

I am familiar with the C Rationale documents, both the C89
original document (which appears to be n802.pdf) and the later
C99 document (C99RationaleV5.10.pdf, dated April 2003). I have a
copy of the n937.pdf document (dated March 2001) but don't recall
looking at it before now (I had already seen the V5.10 version
when I got a copy of n937.pdf from the open-std.org website).

The Rationale documents, and the V5.10 version in particular,
do give explanations for many of the choices made by WG14.
Interesting reading, and sometimes helpful in understanding
what the C standards require as well as why ISO C is the way
it is.

Of course, none of this is in conflict with my statement above
about formal systems, since the Rationale documents are merely
English prose, without giving any sort of formal specification.
The C standard says "what", the Rational documents say "why".

Stefan Monnier <monnier@iro.umontreal.ca> writes:

[...]

You have misconstrued my comments.

According to Tim Rentsch <tr.17687@z991.linuxsc.com>:
>Ivan Godard <ivan@millcomputing.com> writes:
>
>> On 3/9/2022 1:47 PM, Tim Rentsch wrote:
>>
>>> [...] (Disclaimer: what little I know about Mary is from its
>>> wikipedia article; my efforts to locate anything more
>>> substantial have been unsuccessful.)

Worldcat finds six copies in university libraries in North
America and Europe:

https://www.worldcat.org/title/mary-textbook/oclc/25754504

--
Regards,
John Levine, johnl@taugh.com, Primary Perpetrator of "The Internet for Dummies",
Please consider the environment before reading this e-mail. https://jl.ly

John Levine wrote:
> According to Tim Rentsch <tr.17687@z991.linuxsc.com>:
>> Ivan Godard <ivan@millcomputing.com> writes:
>>
>>> On 3/9/2022 1:47 PM, Tim Rentsch wrote:
>>>
>>>> [...] (Disclaimer: what little I know about Mary is from its
>>>> wikipedia article; my efforts to locate anything more
>>>> substantial have been unsuccessful.)
>
> Worldcat finds six copies in university libraries in North
> America and Europe:
>
> https://www.worldcat.org/title/mary-textbook/oclc/25754504
>

There are a bunch of early 1970's ACM papers by Mark Rain on Mary

[paywalled]
https://dl.acm.org/profile/81100175004/publications?Role=author

and Stanford claims to have a copy of the users guide
for suitably privileged faculty, staff, or students.

Mary. Users documentation
Rain M., Conradi R., Holager P., 1973
https://searchworks.stanford.edu/view/4596977

According to EricP <ThatWouldBeTelling@thevillage.com>:
>There are a bunch of early 1970's ACM papers by Mark Rain on Mary
>
>[paywalled]
>https://dl.acm.org/profile/81100175004/publications?Role=author

Here's some of them:

http://archive.computerhistory.org/resources/text/algol/algol_bulletin/A34/P42.HTM

http://archive.computerhistory.org/resources/text/algol/algol_bulletin/A35/P46.HTM

http://archive.computerhistory.org/resources/text/algol/algol_bulletin/A35/P47.HTM

--
Regards,
John Levine, johnl@taugh.com, Primary Perpetrator of "The Internet for Dummies",
Please consider the environment before reading this e-mail. https://jl.ly

John Levine <johnl@taugh.com> writes:

> According to Tim Rentsch <tr.17687@z991.linuxsc.com>:
>
>> Ivan Godard <ivan@millcomputing.com> writes:
>>
>>> On 3/9/2022 1:47 PM, Tim Rentsch wrote:
>>>
>>>> [...] (Disclaimer: what little I know about Mary is from its
>>>> wikipedia article; my efforts to locate anything more
>>>> substantial have been unsuccessful.)
>
> Worldcat finds six copies in university libraries in North
> America and Europe:
>
> https://www.worldcat.org/title/mary-textbook/oclc/25754504

Yes, I saw that already. But thank you.

EricP <ThatWouldBeTelling@thevillage.com> writes:

> John Levine wrote:
>
>> According to Tim Rentsch <tr.17687@z991.linuxsc.com>:
>>
>>> Ivan Godard <ivan@millcomputing.com> writes:
>>>
>>>> On 3/9/2022 1:47 PM, Tim Rentsch wrote:
>>>>
>>>>> [...] (Disclaimer: what little I know about Mary is from its
>>>>> wikipedia article; my efforts to locate anything more
>>>>> substantial have been unsuccessful.)
>>
>> Worldcat finds six copies in university libraries in North
>> America and Europe:
>>
>> https://www.worldcat.org/title/mary-textbook/oclc/25754504
>
> There are a bunch of early 1970's ACM papers by Mark Rain on Mary
>
> [paywalled]
> https://dl.acm.org/profile/81100175004/publications?Role=author

I looked at this but didn't pursue it after seeing the
followup from John Levine.

> and Stanford claims to have a copy of the users guide
> for suitably privileged faculty, staff, or students.
>
> Mary. Users documentation
> Rain M., Conradi R., Holager P., 1973
> https://searchworks.stanford.edu/view/4596977

Ah. A different work than the Mary textbook, which Stanford
also has. Unfortunately not accessible to me, but thank you.

John Levine <johnl@taugh.com> writes:

> According to EricP <ThatWouldBeTelling@thevillage.com>:
>
>> There are a bunch of early 1970's ACM papers by Mark Rain on Mary
>>
>> [paywalled]
>> https://dl.acm.org/profile/81100175004/publications?Role=author
>
> Here's some of them:
>
> http://archive.computerhistory.org/resources/text/algol/algol_bulletin/A34/P42.HTM
>
> http://archive.computerhistory.org/resources/text/algol/algol_bulletin/A35/P46.HTM
>
> http://archive.computerhistory.org/resources/text/algol/algol_bulletin/A35/P47.HTM

Great! Not a complete reference but enough to answer some
basic questions, which for now will suffice.

My thanks again to Eric and John for their help (and Eric,
I love your email address - be seeing you).

On 3/11/2022 8:58 AM, Tim Rentsch wrote:
> John Levine <johnl@taugh.com> writes:
>
>> According to EricP <ThatWouldBeTelling@thevillage.com>:
>>
>>> There are a bunch of early 1970's ACM papers by Mark Rain on Mary
>>>
>>> [paywalled]
>>> https://dl.acm.org/profile/81100175004/publications?Role=author
>>
>> Here's some of them:
>>
>> http://archive.computerhistory.org/resources/text/algol/algol_bulletin/A34/P42.HTM
>>
>> http://archive.computerhistory.org/resources/text/algol/algol_bulletin/A35/P46.HTM
>>
>> http://archive.computerhistory.org/resources/text/algol/algol_bulletin/A35/P47.HTM
>
> Great! Not a complete reference but enough to answer some
> basic questions, which for now will suffice.
>
> My thanks again to Eric and John for their help (and Eric,
> I love your email address - be seeing you).

Mary1 was done at NTH in Norway, targeting the NDE Nord-1 and Kongsberg
SM-3 and SM-4, similar 16-bit minicomputers used in embedded work, under
an OS written in Mary. The most widespread use was in telephone
exchanges; at one time the telephone system of the PRC ran on NDE
machines with both OS and apps written in Mary.

Mary2 was done at PRC in the US, targeting the DG Nova 1200 and related
ISAs, and the Gould SEL-32. The Nova compiler worked and was
self-hosting, but the Gould target was incomplete and the language never
saw significant commercial use.

According to Ivan Godard <ivan@millcomputing.com>:
>Mary1 was done at NTH in Norway, targeting the NDE Nord-1 and Kongsberg
>SM-3 and SM-4, similar 16-bit minicomputers used in embedded work, under
>an OS written in Mary. The most widespread use was in telephone
>exchanges; at one time the telephone system of the PRC ran on NDE
>machines with both OS and apps written in Mary.
>
>Mary2 was done at PRC in the US, targeting the DG Nova 1200 and related
>ISAs, and the Gould SEL-32. The Nova compiler worked and was
>self-hosting, but the Gould target was incomplete and the language never
>saw significant commercial use.

Mary looks to me like a clever approach to problems that nobody cares about
any more, getting fast code out of tiny compilers on tiny machines. It also
is a lot like "lil" which PJ Plaugher wrote in the 1970s. It was related to
C much as Mary was to algol68 and PL360 to Algol W, sort of a C flavored
assembler. As the author said, it failed because every time there appeared to
be place to use it, they could just fix the C compiler.

http://www.ultimate.com/phil/lil/lil.html

--
Regards,
John Levine, johnl@taugh.com, Primary Perpetrator of "The Internet for Dummies",
Please consider the environment before reading this e-mail. https://jl.ly

Ivan Godard wrote:
> On 3/11/2022 8:58 AM, Tim Rentsch wrote:
>> John Levine <johnl@taugh.com> writes:
>>
>>> According to EricP  <ThatWouldBeTelling@thevillage.com>:
>>>
>>>> There are a bunch of early 1970's ACM papers by Mark Rain on Mary
>>>>
>>>> [paywalled]
>>>> https://dl.acm.org/profile/81100175004/publications?Role=author
>>>
>>> Here's some of them:
>>>
>>> http://archive.computerhistory.org/resources/text/algol/algol_bulletin/A34/P42.HTM
>>>
>>>
>>> http://archive.computerhistory.org/resources/text/algol/algol_bulletin/A35/P46.HTM
>>>
>>>
>>> http://archive.computerhistory.org/resources/text/algol/algol_bulletin/A35/P47.HTM
>>>
>>
>> Great!  Not a complete reference but enough to answer some
>> basic questions, which for now will suffice.
>>
>> My thanks again to Eric and John for their help (and Eric,
>> I love your email address - be seeing you).
>
> Mary1 was done at NTH in Norway, targeting the NDE Nord-1 and Kongsberg
> SM-3 and SM-4, similar 16-bit minicomputers used in embedded work, under
> an OS written in Mary. The most widespread use was in telephone
> exchanges; at one time the telephone system of the PRC ran on NDE
> machines with both OS and apps written in Mary.

In hindsight I found it quite interesting that you had Norway and Sweden
developing Mary and Erlang, both intended for the same telephony work.

A few decades later you had Norwegian researchers inventing the GSM cell
phone standard, but with Sweden and Finland reaping most of the
financial benefits.

Terje

--
- <Terje.Mathisen at tmsw.no>
"almost all programming can be viewed as an exercise in caching"

On 3/12/2022 3:46 AM, Terje Mathisen wrote:
> Ivan Godard wrote:
>> On 3/11/2022 8:58 AM, Tim Rentsch wrote:
>>> John Levine <johnl@taugh.com> writes:
>>>
>>>> According to EricP  <ThatWouldBeTelling@thevillage.com>:
>>>>
>>>>> There are a bunch of early 1970's ACM papers by Mark Rain on Mary
>>>>>
>>>>> [paywalled]
>>>>> https://dl.acm.org/profile/81100175004/publications?Role=author
>>>>
>>>> Here's some of them:
>>>>
>>>> http://archive.computerhistory.org/resources/text/algol/algol_bulletin/A34/P42.HTM
>>>>
>>>>
>>>> http://archive.computerhistory.org/resources/text/algol/algol_bulletin/A35/P46.HTM
>>>>
>>>>
>>>> http://archive.computerhistory.org/resources/text/algol/algol_bulletin/A35/P47.HTM
>>>>
>>>
>>> Great!  Not a complete reference but enough to answer some
>>> basic questions, which for now will suffice.
>>>
>>> My thanks again to Eric and John for their help (and Eric,
>>> I love your email address - be seeing you).
>>
>> Mary1 was done at NTH in Norway, targeting the NDE Nord-1 and
>> Kongsberg SM-3 and SM-4, similar 16-bit minicomputers used in embedded
>> work, under an OS written in Mary. The most widespread use was in
>> telephone exchanges; at one time the telephone system of the PRC ran
>> on NDE machines with both OS and apps written in Mary.
>
> In hindsight I found it quite interesting that you had Norway and Sweden
> developing Mary and Erlang, both intended for the same telephony work.

U. Gothenburg ported Mary1 to 360, so there was a Swedish connection
there too. For that matter, Scandinavia has always hit way above its
population in the language design field: large parts of Algol, Simula,
etc. The other hotbed of language work was Netherlands.

In contrast, very little from the US. That the most widespread languages
of today derive primarily from the US reflects money and politics, not
technical advances.

Theo <theom+news@chiark.greenend.org.uk> writes:
>EricP <ThatWouldBeTelling@thevillage.com> wrote:
>> Yes, that makes sense.
>> Even for a mid-80's TTL DRAM controller I would be
>> surprised if it didn't have same-row detection.
>> Its a few latches and xors.
>>
>> So you are saying that because LDM/STM do a single instruction fetch,
>> then a sequence of data addresses, it allows same-row detection
>> and just a column address strobe CAS will do.
>> For a sequence of individual LD or ST, the instruction addresses
>> would most likely be to a different row than their data addresses
>> so same-row detect doesn't kick in, and requires full RAS and CAS.
>
>Yes. So a traditional LD/ST (even if to contiguous addresses) gives you:
>
>row(instr. fetch); col(IF); row(data0); col(data0);
>row(instr. fetch); col(IF); row(data1); col(data1);
>...
>row(instr. fetch); col(IF); row(data15); col(data15);
>
>whereas STM/LDM has:
>
>row(IF); col(IF); row(data0); col(data0);
>col(data1);
>...
>col(data15);
>
>I'm not very familiar with 1980s DRAMs but I don't think they had multiple
>banks so you could have several rows open at once.

Yes, I don't think they had multiple banks.

I recently revisited memory copying on a 6502: It took ~15
cycles/byte (i.e., 66kB/s on a C64).

The first ARM could use 12 registers for copying (1 PC, 1 source, 1
destination, 1 limit), so copying 48 bytes took 15+15+1+2 cycles (1
for subtract/compare, 2 for the branch; ARM experts will correct me if
that does not work out), i.e., 0.69 cycles/byte (a little less with
unrolling), about 22 times faster than the 6502 at the same clock rate
(and the clock rate was faster). Not bad.

- anton
--
'Anyone trying for "industrial quality" ISA should avoid undefined behavior.'
Mitch Alsup, <c17fcd89-f024-40e7-a594-88a85ac10d20o@googlegroups.com>

Ivan Godard <ivan@millcomputing.com> writes:
>On 3/9/2022 10:00 AM, Anton Ertl wrote:
>> Ivan Godard <ivan@millcomputing.com> writes:
>>> On 3/7/2022 12:19 AM, Anton Ertl wrote:
>>>> I think that type systems are an area where formal descriptions are
>>>> relatively close to being good enough to being used. The main problem
>>>> is that every programming language has its own type system with its
>>>> own twists, that results in its own notation. There is no unifying
>>>> notation like (E)BNF or stack effect notation that is usable for
>>>> describing many languages.
....
>> But we have no successful formal notation for type systems.
>
>Depends on what "successful" means :-) If "does the job" then we have
>some.

In the present context it means R>1; i.e., other language designers
get infected with the notation and use it for their language,
eventually resulting in a significant portion of programming languages
using this notation. We have no such notation for type systems.

- anton
--
'Anyone trying for "industrial quality" ISA should avoid undefined behavior.'
Mitch Alsup, <c17fcd89-f024-40e7-a594-88a85ac10d20o@googlegroups.com>