Jonathan S. Shapiro wrote:
> I am coming to the reluctant conclusion that BitC needs a limited form
> of conditional compilation system. Let me give two illustrations of the
> problem:
>
> 1. Arch-dependent alignment
> 2. Debugging Elision
>
> Now both of these use cases boil down to setting some constant value and
> then writing code that is conditional on that value. This can be handled
> through the module include system.
I agree.
> The case that scares me more is the case where platform dependencies
> force us to change the type signatures of procedures. For example, the
> seek() system call on a 64-bit filesystem platform has a different
> signature than the one on a 32-bit filesystem platform.
I think what you are saying here is that we can parametrize functions
over layout, alignment, etc., but this will complicate their signatures?
For example: we could have
seek: (forall (fs 'b) (fn ('b) ()))
Different implementations will supply different instances for seek:
(definstance (fs int32) ...)
(definstance (fs int64) ...)
However, this might result in complicated function/interface signatures
in general, because of multiple parameters like architecture,
endian-ness, file-system, etc.
> The problem with
> these cases is that they touch the type system, and that raises issues
> about type propagation, inference, and compatibility.
This is definitely true. Since layout/alignment constraints are not
syntax directed, I think that they will increase the amount of
annotations that the user must provide in general. The inference system
will propagate types and constraints, but (more detailed) annotations
will be necessary at declarations and interfaces. I think that the
compatibility issues are similar to mutability -- it is just that there
are more atomic labels in this case.
The following paper uses a type/effect system for parameterizing C-like
programs over low-level layout/alignment constraints:
``A Theory of Platform-Dependent Low-Level Software'': Marius Nita,
Dan Grossman, and Craig Chambers
http://www.cs.washington.edu/homes/djg/papers/tpdlls.pdf
I have not read the paper completely. It describes the logical type
system that produces layout constraints for a simple subset of C
(basically a sequence of statements and loops). Trying to infer these
constraints will either have to be done on the whole program, or require
detailed type+effect annotations.
In a way, this problem can be partially alleviated by using conditional
compilation. For example, we already have support for the most trivial
form of architecture dependent conditional compilation in the form of
`word' type, which varies by architecture.
A similar approach is proposed in
``Automatic Transformation of Bit-Level C Code to Support Multiple
Equivalent Data Layouts'': Marius Nita and Dan Grossman
http://www.cs.washington.edu/homes/djg/papers/nita-cc08.pdf
In their system, programmers write code assuming a particular data
layout, but specify how different layouts of the same data relate to
each other. A translation tool generates code for the others layouts.
Swaroop.
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev
