Future of Linux (.so contracts)

[Bruce Stephens]

Davide Bolcioni <davide.bolcioni at 3di.it> writes:

> If we say a library is a collection of functions which have a
> signature and an implementation, the notion of change becomes: 1 -
> an implementation change which preserves the signature; 2 - a
> signature change (which may be construed as a deletion followed by
> an addition, so anybody expecting to find the old function should
> not find it) which almost always implies an implementation change;
> 
> The problem, of course, is that we check the signature but care
> about the implementation (in the sense that we call a function for
> what it does, although we should not rely on the exact means it uses
> to get the job done). The implementation includes considerations
> such as efficiency, i.e. application chose a function with more
> limited functionality because it was more efficient, so
> implementation goes into the contract in multiple ways (which is
> inconvenient).

I'm probably going off at a bit of a tangent, but it strikes me that a
potentially useful tool is parts of TenDRA
<URL:http://alph.dra.hmg.gb/TenDRA/>.  TenDRA as a practical compiler
probably isn't interesting---I suspect egcs beats it (although
compiling with more than one compiler is useful for checking
portability beyond gcc, of course)---from the point of view of
checking portability, or checking signature of APIs, TenDRA provides
some features which look nice, however.

With the TenDRA compiler, I can compile the etags.c from XEmacs, and
be pretty sure that it requires only features (as in headers, types,
macros, functions) provided by ISO C and POSIX:

	% tcc -Yposix -c etags.c

Even if the compiler itself is ignored, TenDRA provides a language a
little more subtle than C header files for specifying what an API
provides.  For example, you can specify that a struct typedef has
certain elements, but does not say which order they'll come in (and
the compiler can check that a program does not try to assume an
ordering).

In a sense, perhaps this is too much subtlety for programs to be
shipped in binary: if my glibc implements some important struct
differently to yours, then no amount of fiddling is going to get your
binary to work on my machine.  But for checking (syntactic
only---there's nothing about semantics involved) portability of
source, this strikes me as useful.

Indeed, just writing down (in this already defined language) suitable
definitions of APIs would surely be handy for a number of uses.  The
formalism strikes me as a little clearer to read than header files, in
that it strips out implementation details, making the interface that
I'm supposed to use more visible.

Here's a few excerpts for apis/ansi/stdio.h, the definition of what
ANSI C stdio.h provides:

	+SUBSET "file" := { +TYPE FILE ; } ;

	+EXP FILE *stdin, *stdout, *stderr ;
	+SUBSET "eof" := { +CONST int EOF ; } ;

This says that FILE is a type, but says nothing else about it.
Similarly, EOF is a constant int.  The SUBSET things indicate that
other APIs and other header files may reference these subsets of
stdio.h without importing the whole lot, I think.

	+IFNDEF __JUST_POSIX
	+IFNDEF __JUST_XPG3
	+TYPE fpos_t ;
	+FUNC int fgetpos ( FILE *, fpos_t * ) ;
	+FUNC int fsetpos ( FILE *, const fpos_t * ) ;
	+ENDIF
	+FUNC int setvbuf ( FILE *, char *, int, size_t ) ;
	+FUNC int vfprintf ( FILE *, const char *, ~va_list ) ;
	+FUNC int vprintf ( const char *, ~va_list ) ;
	+FUNC int vsprintf ( char *, const char *, ~va_list ) ;
	+ENDIF

Declarations of functions.  Fairly obvious, I suspect.  (~va_list is
declared elsewhere.)

Does this kind of writing down of APIs strike anybody else as useful,
or am I just insane?