[TALK] Proving fundamental Unix guarantees

[Warren Toomey]

On Mon, Jun 30, 2003 at 04:19:15PM +1000, Gary Schmidt wrote:
> Well, since the folk who _really_ know the answer, at great length, are obviously still tied up in End-Of-Financial-Year crud, I'll try to remember more...

Time for my $0.05 worth.

A program image on disk consists of those areas which must be stored. So:

text area: holds the code of the program
data area: holds the initialised global data
symbol table: optional
list of required shared libraries: optional

Nothing else needs to be stored. However, the size of the BSS must be
stored.

When the program is executed, the text and data areas are loaded into
memory (and let's ignore demand paging for now). The process also
has these areas:

BSS: holds global data which was not initialised in the source code.
     Normally this is set to zero, and this is the question we're all
     trying to answer.
Heap: the process' global data. Size can be varied using sbrk() or brk()
Stack: the process' local data, also used for function parameters and
	return addresses.

I can't find an answer to the question of whether BSS is initialised.
The 7th Edition manual says that BSS is set to 0s (see a.out(5)). I've
checked other references but they don't explicitly state this:
	- Harbison & Steele, C: A Reference Manual
	- Rochkind, Advanced UNIX Programming
	- Stevens, Advanced Programming in the UNIX Environment
	- Koenig, C Traps and Pitfalls
	- Ritchie, The C Programming Language 1st Edition
	- A draft of the POSIX standard I have in a folder

It would be worth reading your OS manuals on a.out and ELF. FreeBSD says
in a.out(5):

     a_bss     Contains the number of bytes in the `bss segment' and is used
               by the kernel to set the initial break (brk(2)) after the data
               segment.  The kernel loads the program so that this amount of
               writable memory appears to follow the data segment and ini-
               tially reads as zeroes.  (bss = block started by symbol)

and in elf(5):

     .bss       This section holds uninitialized data that contributes to the
                program's memory image.  By definition, the system initializes
                the data with zeros when the program begins to run.  This sec-
                tion is of type SHT_NOBITS.  The attributes types are

and in execve(2):

     An executable object
     file consists of an identifying header, followed by pages of data repre-
     senting the initial program (text) and initialized data pages.  Addi-
     tional pages may be specified by the header to be initialized with zero
     data;  see elf(5) and a.out(5).

Has anybody checked the Single UNIX specification? The latest ANSI C standard?

	Warren