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. > 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. I also considered dirty tricks in which unsafe code would reach in and manipulate the tag headers for objects directly, but this is both non-portable and unreliable. The location of the tag header is implementation dependent, the strategy doesn't work for arrays of unboxed unions, and in any case nothing in CLR that I can see precludes a tagless collector. Perhaps somebody here knows more about CLR than I do, and can suggest an option that I do not see. That would be quite wonderful. shap _______________________________________________ bitc-dev mailing list [email protected] http://www.coyotos.org/mailman/listinfo/bitc-dev
