64
edits
Tamarin:WeeklyUpdates: Difference between revisions
no edit summary
No edit summary |
No edit summary |
||
| Line 28: | Line 28: | ||
== Updates == | == Updates == | ||
=== Meeting Logistics (Leslie)=== | === Meeting Logistics (Leslie)=== | ||
* Weekly meetings to move to Tuesdays at 1:00 ET starting next week, 11/18 | |||
* Details to be sent to list and updated on the wiki by the end of this week. | |||
=== Verifying the Code Generator (Jim Blandy)=== | |||
* Jim came up with this idea while watching Andreas hunt down bugs in TraceMonkey | |||
* The verifier would pass over the code and verify that all operations being performed are being done on appropriate types | |||
* We have a type map that shows what kinds of values are in what places. The verifier would propagate those types forward and it would know the layout of the object. If we found ourselves arriving at some type info, we could verify the type map. | |||
* Reference: George Necula's Proof Carrying Code project | |||
** Provides type annotations for arbitrary machine code. Interesting thing, he found that he caught lots and lots of compiler bugs. | |||
* If the verifier had a type system that was sound, we could ensure that the compiler was not generating code that was unsound. | |||
* Here is the bug associated with this idea: [Bug 463137|https://bugzilla.mozilla.org/show_bug.cgi?id=463137] _TM: TraceMonkey should verify the compiler's output_ | |||
=== Proposal on Creating a Shared NJ Repository (Edwin)=== | === Proposal on Creating a Shared NJ Repository (Edwin)=== | ||