Revision as of 15:45, 12 November 2008

These updates concern Tamarin and related projects only.

Meeting Details

2:00pm Pacific Time (21:00 UTC) on Tuesdays
- (5PM Eastern US, 11PM Oslo, 6AM (Wed) Seoul, 7AM (Wed) Melbourne)
Location: Tel: 866 705 2554 (us), 913 227 1201 (int’l)
- Passcode: 914008
Duration: 60 minutes
join irc.mozilla.org #tamarin for attendence taking and questions

Next meeting's Agenda Items:

November 11, 2008

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_

@@ Line 28: / Line 28: @@
 == Updates ==
 === 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_
-=== Verifying the Code Generator (Jim Blandy)===
 === Proposal on Creating a Shared NJ Repository (Edwin)===