lkuper / dissertation Goto Github PK

See my notes on the reviews for some of the justification for this change.

I think it actually won't be that much work to update the existing lambdaLVar determinism proof to accommodate arbitrary update operations. In fact, I don't think there's even any more proving to do; it's just a matter of rearranging things I've already written. Famous last words, maybe...

Reviewer 2 explicitly asked how we'd handle parallel or (and short-circuit computations in general). This section's already in my dissertation (although it's about parallel and instead of parallel or); I just need to include it here too.

Checklist:

• Move arbitrary updates over to lambdaLVar (issue #3) (@lkuper)
• Systematic presentation of LVish API (issue #6) (@rrnewton)
• Resolve question about consistent termination (issue #7) (???)
• Add stuff about early termination and parallel or (issue #4) (@lkuper)
• Tone down the claim that we subsume KPNs (issue #5) (@rrnewton)
• Address copy edits and minor stuff from both reviews (@lkuper -- in progress)
• Write a cover letter to go with our revised paper, explaining what revisions we did and didn't do. (@lkuper -- in progress)

We don't need to show the entire API, but in addition to the series of examples in section 4.2, we should give a systematic presentation of the most important API types and operations that we provide (not necessarily the stuff that data structure implementors would use, but the stuff that application writers would use). Hopefully a lot of this is in the LVish 2.0 Haddocks anyway.

• The month and year on your title page should be the month and year in which the degree will actually be awarded. Please change the month and year on your title page to September 2015.
• On the abstract page, your name should be place as the first item on the page, centered. Under your name should be the dissertation title, either in all capital letters or underlined. Remove your name after the title.
• Black font should be used throughout the dissertation with the only exception being areas where a different font color serves a purpose in explaining or highlighting some aspect of the research/dissertation in a way black font could not. Change all non-black font which serves no other purpose to black font.
• Add an entry for your curriculum vita (CV) to the table of contents. The CV should be the last item in your dissertation and listed last on the table of contents. Since CV pages should not have a page number, the table of contents entry for it should note only the presence of the CV at the end with no page number indicated.
• Remove all blank pages from the dissertation.
• Remove the small heading from page 135 or place it on all the bibliography pages. It is not used on other bibliography pages and we ask that formatting be consistent throughout.
• On the CV, remove the header and page number. CV pages are not numbered and headers are not used in dissertations. Change the month of your PhD to September on the CV.

From reviewer 2's review:

It is rather unfortunate that the determinism result (Theorem 2.1)
specifically does not address consistent termination (i.e., that if
one run terminates with a non-error result, another run cannot
diverge), but that this is only left as a conjecture. I think that,
especially for an archival publication, the conjecture ought to be
resolved (presumably positively), or there should at least be given a
clear argument for why such a resolution would be a particularly hard
undertaking, beyond the reasonable scope of the paper.

Note that the determinism theorem already establishes a very tight
correspondence between different runs of a program: any two
successfully terminated computations from the same starting
configuration must yield stores that differ only by a permutation on
the locations, and so in particular, the two runs must have performed
equally many allocations. Since any program can be peppered with
additional dummy allocations, this effectively means that all
successful runs of a program perform the same number of basic
operations, only perhaps in a different order. Given this, it seems
particularly unlikely that one could construct a scenario in which one
run terminates successfully after n transition steps, while another
performs even n+1, let alone infinitely many, such steps.

Both reviewers brought this up. It's true that the claim is a bit strong!

This is mentioned in both the intro and the conclusion, if not in other places.