[gambit-list] Gambit compiler is deterministic right?

Adam adam.mlmb at gmail.com
Fri Mar 15 14:26:32 EDT 2019


I would mean that different calls to |compile-file| within the same
invocation of gsc, generates the exact character comparison of generated .c
/ binary backend output file for a given Scheme file and its included
dependencies, maybe presuming some optional |compile-file| argument(s) to
force determinism.


The usecase I had in mind is validation of authenticity of binaries:

A person or automated build script would be able to validate that a given
binary executable (e.g. with hash X) corresponds to an exact given code
base (e.g. with hash Y) built on a given exact compiler/build/OS
environment (e.g. with hash Z or other unique identifier).

This could be instrumental for validation before cryptographic signing e.g.
multiple participants certify that a binary is authentic, or other code
review processes or security audits.


Thanks for pointing out the various ways in which achieving this is
non-trivial. Right so sources of nondeterminism include
 * Any timestamp included by the compiler in the compile output (would need
to be removed, set to the file's creation time, or zero, or such),
 * Filename included by the compiler in the compile output (would need to
be forced somehow),
 * Gensym,
 * Undeterministic macros in user's code,
 * (and CC/AS nondeterminism).

If the determinism would be broken or break at some point, builds would
simply yield non-matching hashes, and an effort would need to be undertaken
by all participants to figure out why, and that could be both obvious stuff
in the user code (like the nondeterministic |stamp| macro example you
provided) or some unintentional reason which probably not but still could
lie in the compiler.


If I read you right, the compiler is expectably mostly
deterministic-proofed already, but this has not been a stressed design goal
and may need some tweaking both generally and for a given codebase.

This was mostly what I thought you would say however your confirmation made
all difference.

Thank you for all your clarifications!

Adam

On Fri, 15 Mar 2019 at 19:47, Marc Feeley <feeley at iro.umontreal.ca> wrote:

> But what does it mean for the compiler to be deterministic?
>
> - deterministic for different invocations of gsc, or for different calls
> of compile-file within the same invocation of gsc (gensym would only
> potentially be an issue in the second case)
>
> - exact character comparison of generated .c file for a given Scheme file
> and its include dependencies
>
> - same .c code generated regarless of file name and location in the
> filesystem (it is already not the case if the file names are different, and
> with -debug the location in the filesystem is an issue)
>
> - same .c code for each top-level Scheme definition, but possibly not same
> ordering of those definitions
>
> - same ordering of all the lines of .c code, but possibly different names
> for local labels, local variables, etc
>
> - different ordering of the instructions in the code (i.e. ordering of
> labels), but same semantics
>
> - same generated machine code from gcc for a given Scheme file
>
> What is your use-case and which definition of compiler determinism are you
> looking for?
>
> In my coding style I try to avoid nondeterministic behavior, but I have no
> proof that there isn’t some nondeterminism left.
>
> Thread preemption interrupts are particularly nasty because they may cause
> continuations to be captured in subtly different ways, which can lead to
> the stack area overflowing sooner or later, which impacts when GCs are
> triggered, which impacts where objects are allocated, which affects the
> collisions in eq? hash tables, which affects the ordering of table->list
> (which is used in a couple places in the compiler, but fortunately it seems
> the resulting list is then explicitly sorted).  Anyway, you get the idea
> that it is non-trivial to prove the strictess level of deterministic
> behavior (exact same generated .c code).
>
> Marc
>
>
>
> > On Mar 15, 2019, at 1:02 AM, Adam <adam.mlmb at gmail.com> wrote:
> >
> > Hi Marc,
> >
> > I meant except for nondeterministic behavior caused by macros, so your
> example below is excluded from the definition.
> >
> > The compiler uses gensym a lot, this would be a primary cause of
> nondeterminism wouldn't it, so for instance if thread-safe determinism
> would be desired, the Gambit user would need to implement a thread-local
> gensym, correct?
> >
> > (This would exclude thread preemption interrupts and GC as sources of
> nondeterminism - thread preemption and GC would only effect |compile-file|
> in the way that it could affect the order of gensym calls, right?)
> >
> > Oh hashtables as a source of |compile-file| nondeterminism, interesting
> - what does |compile-file| use hashtables for?
> >
> > Thanks!!
> > Adam
> >
> > On Fri, 15 Mar 2019 at 12:55, Marc Feeley <feeley at iro.umontreal.ca>
> wrote:
> > You’ll have to define what it means for the compiler to be
> deterministic.  Do you expect the compilation of the following program to
> yield the same executable every time it is compiled?
> >
> > (define-macro (stamp)
> >   (read-line (open-tcp-client "time-a.timefreq.bldrdoc.gov:37")))
> >
> > (pp (string-append "hello! " (stamp)))
> >
> > Macros open a big can of worms…
> >
> > If you avoid macros the compiler is probably mostly deterministic… but I
> do not have a proof handy!  Hash tables, GC, thread preemption interrupts,
> etc can introduce nondeterminism that may be observable in some situations.
> >
> > Marc
> >
> >
> > On Tue, 26 Feb 2019 at 09:18, Adam <adam.mlmb at gmail.com> wrote:
> > Hi Marc,
> >
> > Gambit's compiler is deterministic right?
> >
> > (As in Scheme to GVM, GVM to C or binary. Underlying C compiler's
> determinism is a separate matter altogether.)
> >
> > A consideration could be that compilation output is a function of
> |gensym| and therefore its counter must be managed for deterministic
> compilation.
> >
> > Another consideration that if running more instances of the compiler in
> one Gambit process concurrently, the |gensym| calls could have arbitrary
> order and therefore determinism break.
> >
> > Adam
> >
> >       Virus-free. www.avg.com
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mailman.iro.umontreal.ca/pipermail/gambit-list/attachments/20190316/8e4b336c/attachment.htm>


More information about the Gambit-list mailing list