asajeffrey

-- A Demonstration of Agda
--
-- Alan Jeffrey <ajeffrey@bell-labs.com>
--
-- Agda is:
-- * a foundation of mathematics
-- * a programming language
--
-- Foundationally:
-- * Constructive logic

asajeffrey

// API for half-boxes
// These are like boxes, but when you create them, you get two of them,
// and you can get a box back by calling half1.whole(half2).
// It's a run-time error if you ever call  half1.whole(half2) for half-boxes
// which weren't created as a pair.

trait Extractable {}
impl<T> Extractable for Option<T> where T: Extractable {}
impl<T> Extractable for HalfBox<T> {}
impl Extractable for u64 {}

asajeffrey

Uprooting

We root way too much in DOM. Let's not do that.

Magic DOM might fix a lot of problems here, and we're not certain what the performance hit of this is, so we shouldn't really do anything about this until after that. This is more of a dump of all the ideas that came up in this discussion.

Low hanging fruit: Escape analysis

There are lot of .root()s left over from the pre-dereffable-JS<T> era. These are transitively rooted and aren't being moved, so just using Deref should work. Simple escape analysis can catch these.

asajeffrey

$ valgrind --leak-check=full ./target/debug/servo-master -x tests/html/about-mozilla.html 
==5133== Memcheck, a memory error detector
==5133== Copyright (C) 2002-2015, and GNU GPL'd, by Julian Seward et al.
==5133== Using Valgrind-3.11.0 and LibVEX; rerun with -h for copyright info
==5133== Command: ./target/debug/servo-master -x tests/html/about-mozilla.html
==5133== 
==5133== Conditional jump or move depends on uninitialised value(s)
==5133==    at 0x3043686: path::_$LT$impl$GT$::is_dir::hed8e8c2f3b7f9c944im (in /home/ajeffrey/gdrive/scratch/servo/target/debug/servo-master)
==5133==    by 0x229AA24: resource_files::resources_dir_path::heeefbf23f5e70a58ANh (resource_files.rs:39)
==5133==    by 0x22958F6: prefs::read_prefs::h7a9994510ac56d1aveh (prefs.rs:122)

asajeffrey

$ valgrind --leak-check=full ./target/debug/servo -x tests/dromaeo/dromaeo/tests/dom-attr.html 
==5705== Memcheck, a memory error detector
==5705== Copyright (C) 2002-2015, and GNU GPL'd, by Julian Seward et al.
==5705== Using Valgrind-3.11.0 and LibVEX; rerun with -h for copyright info
==5705== Command: ./target/debug/servo -x tests/dromaeo/dromaeo/tests/dom-attr.html
==5705== 
==5705== Conditional jump or move depends on uninitialised value(s)
==5705==    at 0x304B766: path::_$LT$impl$GT$::is_dir::hed8e8c2f3b7f9c944im (in /home/ajeffrey/gdrive/scratch/servo/target/debug/servo)
==5705==    by 0x229CC54: resource_files::resources_dir_path::hd9eeac5458d45061BNh (resource_files.rs:39)
==5705==    by 0x2297B26: prefs::read_prefs::hcb1223650750dcc4weh (prefs.rs:122)

asajeffrey

$ valgrind ./target/release/servo-master http://twitter.com/
==23110== Memcheck, a memory error detector
==23110== Copyright (C) 2002-2015, and GNU GPL'd, by Julian Seward et al.
==23110== Using Valgrind-3.11.0 and LibVEX; rerun with -h for copyright info
==23110== Command: ./target/release/servo-master http://twitter.com/
==23110== 
==23110== Conditional jump or move depends on uninitialised value(s)
==23110==    at 0x1BB49B6: path::_$LT$impl$GT$::is_dir::hed8e8c2f3b7f9c944im (in /home/ajeffrey/gdrive/scratch/servo/target/release/servo-master)
==23110==    by 0x11477AB: resource_files::resources_dir_path::h63eef1cfe6accd1dOLh (in /home/ajeffrey/gdrive/scratch/servo/target/release/servo-master)
==23110==    by 0x1144178: prefs::_$LT$impl$GT$::deref::hb089f63ca6b0673e00g (in /home/ajeffrey/gdrive/scratch/servo/target/release/servo-master)

asajeffrey

$ ./target/release/servo-master http://twitter.com/ & while sleep 1; do cat /proc/$!/statm; done
[1] 26640
1120851 43858 11215 11031 0 1071264 0
1224897 64701 18310 11031 0 1160998 0
1234128 75222 19199 11031 0 1162453 0
ERROR:js::rust: Error at https://abs.twimg.com/c/swift/en/init.671270dc6b028397433710112fead9b41edab227.js:814:87: navigator.plugins is undefined

1298035 96195 20304 11031 0 1221248 0
1298035 96195 20304 11031 0 1221248 0
1298035 96195 20304 11031 0 1221248 0

asajeffrey

The problem at hand is trying to come up with a definition of legal unsafe code for Rust. The context is the Rust memory model. A (probably incomplete) list of goals is:

• Be simple enough, and close enough to common practice that most idiomatic C code which programmers would expect to maintain the Rust memory invariants is legal.
• Support common program optimizations of safe code, by compilers, hardware, or software developers.
• Not allow for undefined behaviour.

The Tootsie Pop model is a simple model of unsafety, based on call boundaries into and out of unsafe code. The model has a temporal flavour,

asajeffrey

abstract class Nope<T extends Nope<T>> {
    private Nope() {}
}

class NopeElim {
    public<T extends Nope<T>> void ohNo() {
        System.out.println("Is there a way to call this");
    }
}

asajeffrey

/* THIS FILE IS AUTOGENERATED - DO NOT EDIT */

#![allow(non_camel_case_types,non_upper_case_globals,unused_imports,unused_variables,unused_assignments)]
use core::nonzero::NonZero;
use dom;
use dom::bindings;
use dom::bindings::callback::CallSetup;
use dom::bindings::callback::CallbackContainer;
use dom::bindings::callback::CallbackFunction;
use dom::bindings::callback::CallbackInterface;