write(f1, "pp");
 write(f2, "qq");

• write block: A write of size block to a file. Two special arguments to write block are zeroes and random: zeroes indicates the file system initializing a newly allocated block to zero; random indicates an uninitialized block. Writes beyond the end of a file cause data to be stored without changing file size.
• change file size: Changes the size of a file inode.
• create dir entry: Creates a directory entry in a directory, and associates a file inode or directory with it.
• delete dir entry: Deletes a directory entry.
• stdout: Adds messages to the terminal output.

open(path="/x2VC") = 10
Micro-ops: None 
Ordered after: None

pwrite(fd=10, offset=0, size=1024)
Micro-ops: #1 write   block(inode=8, offset=0, size=512) 
Micro-ops: #2 write   block(inode=8, offset=512, size=512) 
Ordered after: None

fsync(10)
Micro-ops: None 
Ordered after: None

pwrite(fd=10, offset=1024, size=1024)
Micro-ops: #3 write block(inode=8, offset=1024, size=512) 
Micro-ops: #4 write block(inode=8, offset=1536, size=512) 
Ordered after: #1, #2

link(oldpath="/x2VC", newpath="/file")
Micro-ops: #5 create dir entry(dir=2, entry=‘file’, inode=8) 
Ordered after: #1, #2

write(fd=1, data="Writes recorded", size=15)
Micro-ops: #6 stdout(”Writes recorded”)
Ordered after: #1, #2
/*
Listing 2: Annotated Update Protocol Example. Micro-operations generated for each system call are shown along with their dependencies. The inode number of x2VC is 8, and for the root directory is 2. Some details of listed system calls have been omitted.
*/

ALICE is not complete, in that there may be vulnerabilities that are not detected by ALICE. It also requires the user to write application workloads and checkers; we believe workload automation is orthogonal to the goal of ALICE, and various model-checking techniques can be used to augment ALICE.

Figure 4: Protocol Diagrams. The diagram shows the modularized update protocol for all applications. For applications with more than one configuration (or versions), only a single configuration is shown (SQLite: Rollback, LevelDB: 1.15). Uninteresting parts of the protocol and a few vulnerabilities (similar to those already shown) are omitted. Repeated operations in a protocol are shown as ‘N ×’ next to the operation, and portions of the protocol executed conditionally are shown as ‘? ×’. Blue-colored text simply highlights such annotations and sync calls. Ordering and durability dependencies are indicated with arrows, and dependencies between modules are indicated by the numbers on the arrows, corresponding to line numbers in modules. Durability dependency arrows end in an stdout micro-op; additionally, the two dependencies marked with * in HSQLDB are also durability dependencies. Dotted arrows correspond to safe rename or safe file flush vulnerabilities discussed in Section 4.4. Operations inside brackets must be persisted together atomically.