On Sat, Mar 13, 2010 at 4:47 PM, Jonathan S. Shapiro <[email protected]>wrote:
> On Sat, Mar 13, 2010 at 7:19 AM, Sandro Magi <[email protected]> > wrote: > > > I think most high-level BitC constructs can be expressed as ordinary > > verifiable CIL, it's just the low-level stuff which will be unverifiable. > > Yes. In fact, it looks like the only BitC feature that is unverifiable > in CIL is unboxed unions containing object references. The rest can > all be translated into verifiable CIL terms, though in some cases the > translation is obscure. > Encoding some construct from functional languages like type classes can be quite tricky, specially if the objective is to produce fast code. > > > I think if BitC provided an equally safe yet more expressive > > verification mechanism, that at least backend people would use it... > > If ... a verification pass like Microsoft's verification tool > > could verify their safety, that would be ideal. > > Unfortunately, matters are not that simple. > > In order to run on CLR, there are two requirements you need to be able to > meet: > > 1. Your program needs to be expressible in CIL. Ideally, but not > necessarily, in safe CIL Your proposal above would address the safety > requirement, though it isn't clear that the verifier in CLR (or any > other implementation of CIL) is a safe component. > > 2. Your program needs to be expressible in a way that the CLR runtime > (specifically the GC) can handle. > > Unfortunately, Microsoft does not seem to have given much attention to > GC in an unverified environment. The presumptive purpose of unverified > code seems to have been unmanaged languages. In particular, it appears > that the GC only knows how to interpret types that are expressible in > the verified subset of CTS. I spent some time looking in to this > yesterday. There is a range of possible solutions: > > 1. Somehow inform the GC about how to interpret these types. > Unfortunately, the CLI specification does not appear to make any > provision for this. > 2. Reject unboxed unions containing references as "CLI unsafe". This > is probably the most feasible solution. > 3. Implement all unions containing references as boxed, but implement > the copy semantics of unboxed unions for them. > 4. Give up and compile to unsafe CLI, implementing the garbage > collector by ourselves. At that point the only advantage over LLVM is > the potential for interop. We would lose any/all advantage of the very > mature CLI GC system. > > Off hand, those are the options I see, and of them, I think that [1] > is infeasible and [4] gives us very little advantage that I can see. > There is another option, which is to extend Mono and propose such change to be standardized by ECMA. This is feasible thou might take a couple of years before MS catch up. The CLI type system is not expressible enough to support tag-less safe unions. Mostly because it's undecidable which element is been used without either tags or explicit checks. Support for such safe mixed reference/value type unions is a very desirable feature as it can be used to have a very fast representation of integers in dynamic languages. The Mono community is very welcoming into supporting such improvements.
_______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
