Research.js: Evaluating Research Tool Usability on the Web

Joel Galenson, Cindy Rubio-González, Sarah Chasins, Liang Gong

UC Berkeley

Motivation

• Online demos
• attract users
• generate data

Motivation

• rise4fun [Ball et al 2013]

Motivation

• TouchDevelop [Ball et al 2014]
• See Figure 9.

Motivation

• JSNice [Raychev et al]
• Featured on Slashdot, reddit, Hacker News, ...

Approaches

• Run web server
• Cost, load, security
• VM image
• Hard to attract interest

Emscripten

• LLVM to JavaScript compiler

Our approach

• Compile code to JavaScript and put on the web
• Cost, load, security
• Hard to attract interest

Emscripten

• And many more tools!
• And many more languages!

MiniSat demo

Boolector demo

Hugs demo

Results

• MiniSat, Lingeling, Boolector, Hugs
• Performance: 3x slower
• Binary size: 2x larger
• At most one code and one build line changed

Challenges

• Closed source binaries
• Compile assembly to JS?
• Performance
• Less useful for performance-focused projects
• Emscripten and browsers are improving rapidly
• Difficulty
• Can be tricky to compile

Challenges: Z3

• ∃ x, y. x = y
• SAT
• ∃ x, y. x > y ∧ x = 42
• if (typeof e !== 'number' && e !== 'longjmp') throw e;
  RangeError: Maximum call stack size exceeded

Thanks!

• http://jgalenson.github.io/research.js/
• Questions?