Super Specs & Sub Specs

I want to consider here a sort of information that might be usefully collected and turned into something akin to a specification. Specifications for two sorts of technology have been of great interest to me, computers and programming languages. In both cases such a meta spec would be about some successful technology that might never influence that technology, but might serve some users of that technology.

Super Spec

The super spec would make extra claims, over and above the official spec. I take the language C as an example and indeed the example that led to this idea. I have learned to read the official specs for several languages and that was an effort for each. I have not learned to read the official C spec and thus nothing I say here should be taken to reflect on that spec.

I think that C is specified so as to be neutral regarding whether the host machine is one’s or two’s complement, or sign and magnitude, or even decimal. There is a great deal of C code in use that assumes two’s complement. All of the personal computers and all of the servers, and all the super computer processors that I know of are two’s complement. All of the DSPs I know are as well. I do not claim that the world should never depart from this plan but it would be good to collect some of the of programmer’s expectations for machine architects lest they build machines that reveal too many bugs. Many of these expectations for C may be written as integer valued expression that are expected to yield 1 (true) for arbitrary bindings of the unsigned integer variables therein. P is a constant which is known to the programmer and either 32 or 64. 

2*x == x<<1
((x<<n)>>n == x&(-1>>(P-n))) || n<0
5&3 == 1
-x == 1+~x
(many more)
These are like axioms and imply many others. There are garbage collectors written in C or C++ that compare pointers with memory barriers and such logic can be explained only in terms of addresses being numbers.

Sub-Spec

Here the sub-spec presumes to give accurate and precise information about a technology omitting some of the information in the official spec, yet accurately describing behavior in well defined situations spelled out in the sub-spec. The IBM 701 (1953) had a quite compete 19 page manual. The Aug 2012 combined volumes of the official x86 manual from Intel is 3020 pages and that excludes graphics extensions, electrical and physical characteristics. I believe that a specification of the user mode architecture could be specified in roughly ⅓ of that. Subsets of even that can be very useful for some purposes, for instance a proof of correctness for a simple compiler would need semantics of quite a limited set of user mode commands.

A particularly useful form of sub-spec for x68, and most other processors would be to precisely enumerate the problem mode state of the processor and state plainly that user mode instructions either trap to privileged mode or change only that state. Perhaps that is somewhere in the 3000 pages but I have looked and not found it. That and a sub-spec of the privileged mode instructions could support a proof of correctness (formal or informal) of a kernel.

Sociology

Sub-specs and super-specs would both be ideal wiki projects. A Wiki would invite extensions and counterexamples in common machines. I hope there would come a time where the meaning would be frozen and only clarifications to the meaning be allowed. There are well known problems here that I do not address.

Another sort of claim is that the floating format is IEEE.

In general it would be useful to collect information about which compilers on which machines met certain axioms.

The Territory

Neither sub-specs nor super-specs are to be considered competitors to the real specs, indeed they form a partial ordering in which a spec may include a sub-spec by reference. The official spec is above the sub-specs and below the super-specs in this ordering. Several languages have ‘official subset’ publications which are useful, but they would be useful even if not official. Scheme SRFIs are a good example of super-specs with some of them depending on others, and some competing.

In these terms the AMD processors would be a sub-super-spec of Intel’s and conversely.