search

CakeML / cakeml

CakeML: A Verified Implementation of ML
https://cakeml.org
Other
964 stars 84 forks source link

move register allocator #47

Closed xrchz closed 9 years ago

xrchz commented 9 years ago

should be in a top-level directory (or if necessary under the compiler directory). may also benefit from some cleanup/refactoring.

myreen commented 9 years ago

Part of it should be in a top-level directory and part of it in the compiler directory. As much as possible should be outside the compiler directory.

tanyongkiam commented 9 years ago

I'll do the following:

Register Allocator (graph coloring + analysis) into its own directory and move around the proofs.

Liveness Analysis + SSA form pass into compiler directory (and word_transform)

tanyongkiam commented 9 years ago

Hmm, where should something like is_alloc_var_def (it just means that a variable is 1 MOD 4) go? It is used in both the allocator and inside the word_lang passes.

I guess I could always just expand out the definition or make the same definition it in both places but that might be a bit ugly (word_ssa shouldn't depend on the allocator).

myreen commented 9 years ago

I think it should live in the register allocator directory. The compiler directory will depend on the regsiter allocator anyway. I don't think it matters whether a few extra files depend on allocator. I mean word_ssa is there in order for the allocator to do a good job (and get the calling conventions right).

tanyongkiam commented 9 years ago

More generally, should conventions live in the syntactic compiler definitions or in the proofs (or in a separate file?). e.g. wordLang needs conventions on top of the various "forms" of programs to turn on/off certain things (e.g. expressions)

Edit: I guess the type of conventions that says "this outputs wordLang without expressions" should be part of the proofs while things like is_alloc_var should be part of the syntactic defs (since they are used there).

myreen commented 9 years ago

I would have guessed that the conventions ought to live in the proofs, since the definitions look like deadcode in the syntactic compiler definitions(?).

Let's hear what Ramana thinks.

xrchz commented 9 years ago

Yes, conventions should be in either the semantics or proofs directory (depending on whether they're better thought of as part of the semantics/semantic properties, or whether they're more a feature/invariant of the correctness proof). The only things in the top-level compiler1 directory should be definitions comprising the executable code of the compiler, and very simple properties about them (termination proofs, length of output equals length of input, etc.). Feel free to go with what seems good to you and record your conventions on the wiki (and we can discuss on a case-by-case basis if there's disagreement).

xrchz commented 9 years ago

For the particular things I think Yong Kiam was describing, I probably would have expected them in semantics/wordPropsTheory.

tanyongkiam commented 9 years ago

I just added the register allocator's (syntactic) conventions to semantics/wordProps, it seems a little bit out of place to me now since semantics/ should have (as I understand) things to do with the semantics like the stack swap lemmas.

Since these are invariants generated by compilation phases, I think they should probably be in proof/ under a new file for "initial definitions" rather than be associated with any specific proofs.

Alternatively, I am currently merging the definition of SSA and the allocator into 1 compilation file (word_alloc). I guess the proof scripts could be similarly merged (and also contain the invariants near the start). This would, however, result in a pretty large file (not sure if that is desirable).

xrchz commented 9 years ago

Regarding your first point, I think currently the semantics/*Props theories are also used for properties just about the syntax, so it doesn't feel entirely out of place to me. But I agree it's maybe a little out of place.

I like your alternative suggestion. I don't think a large file is a problem, if its contents are all sufficiently tightly related. There is a point when too large becomes unwieldy to develop and maintain, but I guess you wouldn't be reaching that point yet..

xrchz commented 9 years ago

@tanyongkiam how far did you get with this? what remains to be done?

tanyongkiam commented 9 years ago

Sorry, I think I have moved some definitions around locally (like the previous suggestion) but I haven't got to fixing the proof, will try to do it this weekend.

On Wed, Jul 8, 2015 at 8:19 PM, Ramana Kumar notifications@github.com wrote:

@tanyongkiam https://github.com/tanyongkiam how far did you get with this? what remains to be done?

— Reply to this email directly or view it on GitHub https://github.com/CakeML/cakeml/issues/47#issuecomment-119555986.