[CakeML-dev] Pathological modLang programs

[Ramana Kumar]

I like the 3rd approach you mention. Rather than checking that property
within mod_live, I think you could prove it as a syntactic property of
source_to_mod. (This puts in the same category of other syntactic
properties that are required for later phases and proved to be propagated
by earlier ones.) It sounds like a reasonably simple property to deal with.

On 26 March 2017 at 13:09, Yong Kiam <tanyongkiam at gmail.com> wrote:

> Hi dev,
>
> I've been stuck on mod_live for awhile, the main problem seems to be that
> this is a legitimate modLang program:
>
> val 0 = fn () => Global 1
> val 1 = ...
> val 2 = (Global 0) ()
> ... Global 1 never read here ...
>
> In my current set up, I pass a set of live globals from back to front
> through the list of decs, tracking all the globals that could have been
> read.
>
> In the above fragment, this approach would delete the val 1 = ... line
> because it was never read from back to front. I think only focusing on
> deleting Dletrecs does not solve the problem either.
>
> I have two ways around this:
>
> 1) fallback to a more naive analysis, i.e. walk through all the
> declarations and keep every global that is ever read. This would not be
> able to catch chains of dead globals:
>
> val 0 = ...
> val 1 = Global 0
> val 2 = Global 1
> ... (0,1,2 all dead, but only 2 would be removed)
>
> 2) go to a more complicated one. Not only do I go back to front, but I
> also go front to back and track for each global, the set of globals that it
> can transitively reference. When a global gets added, this analysis would
> have to add all the globals that can be transitively read via that global.
> (so when 0 gets added above, it transitively adds 1).
>
> I didn't particularly like 1 or 2 because 1) seems too naive and 2) seems
> to difficult (having to deal with termination of the transitive addition).
>
> A potential 3rd approach is to essentially type check the entire program
> and only apply the removal [ass if all the globals happen to point in the
> right way. i.e. any dec at position n must only mention globals < n. I
> think that still works in modLang before any complicated knot tying is done.
>
> Does anyone have better suggestions? Or am I missing something important?
>
>
> _______________________________________________
> Developers mailing list
> Developers at cakeml.org
> https://lists.cakeml.org/listinfo/developers
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.cakeml.org/pipermail/developers/attachments/20170326/e6b778e0/attachment-0001.html>