Re: how to make code stay invariant

[Rolf Schumacher <rolf at august dot de>]

Hi, John.

for the first place I found a much simpler solution.
I checked it with gcc -fPIC, and than applied prelink.

Consider a module m1 calling function o2 in module m2.
If we define an interface compilation unit for m2, say m2if,
that implements o2if just calling o2 and m1 is not using
o2 anymore instead of o2if, m1 stays invariant as long
as the interface is invariant. I can do as much "small changes"
to m2 as I like, the checksum of m1 (in memory and on disk)
stays invariant.

in code now, prior to invariance:

m1.c:
#include "m2.h"
int main(void){o2();}

m2.h:
void o2();

m2.c:
#include "m2.h"
void o2() {printf("hello world");}

and now after changes for invariance:

m1.c:
#include "m2if.h"
int main(void){o2if();}

m2if.h:
void o2if();

m2if.c:
#include "m2if.h"
#include "m2.h"
void o2if(){o2();}

m2.h:
void o2();

m2.c:
#include "m2.h"
void o2() {printf("hello world");}

Conclusion:
The object code invariance is gained just by coding rules.
Introduce of object code invariance is applicable even to existing software.
Benefit: all my module tests to m1 apply in the new software
regardless of changes to m2. I haven't to repeat them.

Remark:
For reduction of validation tests of the software product
as a whole against requirements I still need a reliable
impact analysis in order to reduce tests. Invariance doesn't help here.
Code object invariance gives evidence only for code integrity on
the invariant part of the software, nothing more.
However, that's still a lot.

I'll do that!

Thanks for your great help and all the philosophical hints.
I wouldn't have done without even if the resulting solution is that simple.

kind regards

Rolf

John Carter wrote:
> Hmm, you probably should be scanning Miller's handy...
> http://www.dwheeler.com/essays/high-assurance-floss.html
>
> High Assurance (for Security or Safety) and Free-Libre / Open Source
> Software (FLOSS)... with Lots on Formal Methods
>
>
> On Wed, 26 Jul 2006, Rolf Schumacher wrote:
>
> > > Pretty rare, but they happen.
> > We just had to recall projects in an expensive way
> > upon a difference in gcc compiling for SUN
> > and for Intel. (const in parameters)
> > Debuggin was done on a SUN, delivery was for Intel.
>
> Test like you fly, fly what you tested...
>
> But hmm, you said debug not test... So I think there is more to that
> issue than meets the eye...
>
> > In safety critical systems we have to demonstrate (!) 10**-9.
> > For example, systems in an atomic power plant
> > have to be secure to 10**-13 (asaik). They are not allowed to add 
> > more risk.
> > You have to have risk reduction technologies because you can't reach 
> > that
> > figures with software.
>
> I'm reminded of the Bad Old Days when there were MilSpec computers.
>
> Until they realized that the sheer weight of consumer COTS products
> meant that what was available from the corner store was...
> * Way way cheaper.
> * Way way faster.
> * And much more reliable!
>
> Happened again with handheld GPS during the Gulf War. The COTS /
> Consumer GPS's were just so much better than the MilSpec ones (even with
> the delibrate signal fuzzing!!) that they gave up and used the COTS.
>
> The other thought that comes to mind is a variant of a very old joke....
>
> Patient to Doctor, "Doctor! Doctor! I need to be incredibly hugely
> impossibly painfully costly reliable to do this."
>
> Doctor, "Well don't do that then."
>
> > Just the fact that you can think about an error draws the responsibility
> > to give an accepted figure for it: 1. HAZOP, 2. FMEA at least FTA,
> > you do not have any statistics. It hasn't to be real at all in any past.
>
> Wow! That is really Amazing! You are _so_ deep in the Dilbert Zone! Do
> you _ever_ see sunlight there?
>
> http://www.dilbert.com/comics/dilbert/archive/dilbert-20060724.html
>
> > > Some (targets/versions) of the GCC linker do relaxation passes. ie.
> > > Change long jumps to short jumps, change long references to short
> > > offsets. And since the size of the code has shrunk, they do that again,
> > > and again until it converges.
> > Can I switch that off?
>
> Only applies to very few CPU's, don't know which one you are using. I
> met it on the HC12. Search "info gcc" for "relax".
>
> > > Basically you want each module to be a DLL/sharable object so the 
> > > linker
> > > does the absolute minimum of fix ups.
> > >
> > > You also need a strict acyclic dependency graph between the sharable
> > > objects and then link each layer with lower layers.
> > >
> > > Follow the standard tricks to make a sharable object / DLL.
> > Now that's it: I need a link here to update my knowledge.
>
> http://www.dwheeler.com/program-library/Program-Library-HOWTO/x36.html
> http://people.redhat.com/drepper/dsohowto.pdf
>
> In fact Drepper's whole page is a gold mine of detailed info on ELF.
> http://people.redhat.com/~drepper/
>
> In fact I'll make a wild guess....
>
> If you really understood all the niches and corners of ELF, which is
> quite a large and hairy domain, what you want is already in there
> somewhere.
>
> > > You still need the objdump tricks I mentioned to pull just the sections
> > > you care about out.
> > dito
>
> info binutils
>
>
> > What I wanted to tell you is,
> > that you're completely right with the example of the Unix loader
> > separating tasks by means of address space.
> >
> > I have to look at a module as a task that takes messages and respond
> > with messages. As in UML sequence charts.
> >
> > What is the easiest way to implement a messaging system e.g. by macros
> > for programmers that like to use function calls?
>
> Make it simple to use, complex == more lines of code == programmer
> mistakes.
>
> The one we are using involves declaring and packing and unpacking
> structs all over the place. Yuck! Tedious and error prone.
>
> I itch to rewrite using a simple convention that looks like an ordinary
> function declaration, definition and reference.
>
> And then add a bit of Ruby code generation magic to generate a header
> pulled in by the client and a header to be pulled in by the server. Oh,
> and glue it together with a small, possibly entirely non-portable bit of
> C that understands varargs to serialize the arguments across the
> messaging interface.
>
> I bet I can get a huge reduction in code size, much simpler, much more
> reliable and better code.
>
>
> John Carter Phone : (64)(3) 358 6639
> Tait Electronics Fax : (64)(3) 359 4632
> PO Box 1645 Christchurch Email : john.carter@tait.co.nz
> New Zealand
>
> Carter's Clarification of Murphy's Law.
>
> "Things only ever go right so that they may go more spectacularly 
> wrong later."
>
> > From this principle, all of life and physics may be deduced.

Attachment: smime.p7s
Description: S/MIME Cryptographic Signature