[m-dev.] generating verifiable IL

[Fergus Henderson]

I've been thinking about about the issues involved with generating
verifiable IL for the .NET back-end.

There's basically two issues that cause difficulty for verifiability:

	- treatment of nondet code (continuation and environment pointers)

	- tailcalls with byref arguments

There are three different ways of generating code that may be useful:

	1. Generate unverifiable code.

		- allocate nondet environments on the stack

		- use unmanaged pointers for the environment pointers
		  and continuation pointers

		- generate tail calls with byref arguments

	   This approach is maximally efficient, and portable,
	   but not verifiable.

	   This is what the diff I posted earlier does.
	   But there is still a bit of room for improvement:

		- TODO: use "native int" rather than "int32" for
		  the environment pointers and continuation pointers
		  (for portability to 64-bit architectures)

		- TODO: omit the .initlocals (for efficiency)

		- TODO for future VMs: use ECMA function pointer types
		  rather than "int32" for the continuation pointers
		  (this is a code style issue only; using function pointer
		  types improves verifiability, but not enough to actually
		  make the code verifiable).

		  Note that the ECMA spec defines function pointer types,
		  but Microsoft's current implementation doesn't support them.

	2. Generate code which is verifiable on Microsoft's VM.

		- allocate nondet environments on the heap

		- use managed pointers for the nondet environment pointers

		- use delegates for the continuation pointers

		- don't generate tail calls with byref parameters

	   This approach is verifiable and portable, but not maximally efficient.

	   There's still a fair bit we need to do to make our compiler implement
	   this approach:

		- TODO: use delegates (for verifiability)

		- TODO: work around problem with tailcall & byref parameters,
		  e.g. by not emitting tail calls in those cases
		  (for verifiability)

	3. Generate code which *ought* to be verifiable, but which
	   doesn't work on Microsoft's VM.

		- allocate nondet environments on the stack

		- use ECMA function pointer types for continuation pointers

		- use "refany" for environment pointers

	   This approach is verifiable and efficient, but not portable.
	   It would only work on a VM with extensions on the ECMA spec
	   and with a better verifier than the MS implementation:

		- the VM and verifier must allow "refany" in init-only fields
		  of value types

		- the verifier must allow tailcalls with byref parameters

	   It may be worth implementing this approach even in the absence
	   of any VM which supports it because this may give VM implementors
	   some incentive to implement it.

I plan to implement all three approaches, and make them selectable via one or
more compiler options.  Note that all three use different types for the
environment pointers and/or continuation pointers, which means that the calling
convention for nondet procedures will be different in each case.  So these
will have to be compilation model options.

-- 
Fergus Henderson <fjh at cs.mu.oz.au>  |  "I have always known that the pursuit
The University of Melbourne         |  of excellence is a lethal habit"
WWW: <http://www.cs.mu.oz.au/~fjh>  |     -- the last words of T. S. Garp.
--------------------------------------------------------------------------
mercury-developers mailing list
Post messages to:       mercury-developers at cs.mu.oz.au
Administrative Queries: owner-mercury-developers at cs.mu.oz.au
Subscriptions:          mercury-developers-request at cs.mu.oz.au
--------------------------------------------------------------------------