| \begin{tabular}{|l||r||r|r|r||r|r|r|} | |
| \hline | |
| & \multicolumn{1}{c||}{\textbf{CompCert}} & \multicolumn{3}{c||}{\textbf{\sepcomp-LevelA}} & \multicolumn{3}{c|}{\textbf{\sepcomp-LevelB}} \\ | |
| \cline{3-8} | |
| & \multicolumn{1}{c||}{\textbf{(LOC)}} & \multicolumn{1}{c|}{\textbf{Rm}} & \multicolumn{1}{c|}{\textbf{AddD}} & \multicolumn{1}{c||}{\textbf{AddN}} & \multicolumn{1}{c|}{\textbf{Rm}} & \multicolumn{1}{c|}{\textbf{AddD}} & \multicolumn{1}{c|}{\textbf{AddN}} \\ | |
| \hline | |
| \textbf{Total} & 206702 & 318\phantom{0}(0.2\%) & 465 \phantom{0}(0.2\%) & 3392 \phantom{0}(1.6\%) & 372 \phantom{0}(0.2\%) & 1439 \phantom{0}(0.7\%) & 4845 \phantom{0}(2.3\%) \\ | |
| \hline | |
| \hline | |
| \textbf{Compiler \& Verification} & 88451 & 318\phantom{0}(0.4\%) & 465 \phantom{0}(0.5\%) & 1153 \phantom{0}(1.3\%) & 372 \phantom{0}(0.4\%) & 1439 \phantom{0}(1.6\%) & 1726 \phantom{0}(2.0\%) \\ |
I think JMM-05 (https://github.com/jeehoonkang/memory-model-explorer/blob/master/test/jmm-05.test) should be allowed, as contrary to the decision JMM people (and we) made. Here is a series of "standard" optimizations that lead JMM-05 into a program that can clearly output the designated outcome.
By some global analysis, deduce that r2 should be 0 or 1. Thus transform thread 2 into:
r2 = y;
if (r2) {
x = 1
} else {
| (** **** SNU 4190.310, 2016 Spring *) | |
| (** Assignment 03 *) | |
| (** Due: 2016/04/03 23:59 *) | |
| (* Important: | |
| - Do NOT import other files. | |
| - You are NOT allowed to use the [admit] tactic. |
| ./autoconf/configure.ac: AC_MSG_WARN([LLVM will be built thread-unsafe because atomic builtins are missing]) | |
| ./bindings/go/llvm/bitreader.go: "unsafe" | |
| ./bindings/go/llvm/bitreader.go: defer C.free(unsafe.Pointer(cfilename)) | |
| ./bindings/go/llvm/bitreader.go: C.free(unsafe.Pointer(errmsg)) | |
| ./bindings/go/llvm/bitreader.go: C.free(unsafe.Pointer(errmsg)) | |
| ./bindings/go/llvm/dibuilder.go: "unsafe" | |
| ./bindings/go/llvm/dibuilder.go: defer C.free(unsafe.Pointer(file)) | |
| ./bindings/go/llvm/dibuilder.go: defer C.free(unsafe.Pointer(dir)) | |
| ./bindings/go/llvm/dibuilder.go: defer C.free(unsafe.Pointer(producer)) | |
| ./bindings/go/llvm/dibuilder.go: defer C.free(unsafe.Pointer(flags)) |
| #include <cstdio> | |
| using namespace std; | |
| int main() { | |
| setbuf(stdout, NULL); | |
| int nCase; | |
| scanf("%d", &nCase); |
| root@ubuntu:~/dtrace# cc -v | |
| Using built-in specs. | |
| COLLECT_GCC=cc | |
| COLLECT_LTO_WRAPPER=/usr/lib/gcc/x86_64-linux-gnu/4.8/lto-wrapper | |
| Target: x86_64-linux-gnu | |
| Configured with: ../src/configure -v --with-pkgversion='Ubuntu 4.8.4-2ubuntu1~14.04' --with-bugurl=file:///usr/share/doc/gcc-4.8/README.Bugs --enable-languages=c,c++,java,go,d,fortran,objc,obj-c++ --prefix=/usr --program-suffix=-4.8 --enable-shared --enable-linker-build-id --libexecdir=/usr/lib --without-included-gettext --enable-threads=posix --with-gxx-include-dir=/usr/include/c++/4.8 --libdir=/usr/lib --enable-nls --with-sysroot=/ --enable-clocale=gnu --enable-libstdcxx-debug --enable-libstdcxx-time=yes --enable-gnu-unique-object --disable-libmudflap --enable-plugin --with-system-zlib --disable-browser-plugin --enable-java-awt=gtk --enable-gtk-cairo --with-java-home=/usr/lib/jvm/java-1.5.0-gcj-4.8-amd64/jre --enable-java-home --with-jvm-root-dir=/usr/lib/jvm/java-1.5.0-gcj-4.8-amd64 --with-jvm-jar-dir=/usr/lib/jvm-exports/java-1.5.0-gcj-4.8-amd64 --with |
Jeehoon Kang*, Yoonseung Kim*, Chung-Kil Hur*, Derek Dreyer**, Viktor Vafeiadis**
* Seoul National University & ** MPI-SWS
This is the artifact for the POPL 2016 paper: "Lightweight Verification of Separate Compilation".
| Require Export mid_07. | |
| (* problem #08: 30 points *) | |
| (** Easy: | |
| Define a predicate [sorted_min: nat -> list nat -> Prop], where | |
| [sorted_min n l] holds iff the elements in the list [l] is greater | |
| than or equal to [n] and sorted in the increasing order. | |
| **) |
Jeehoon Kang, Chung-Kil Hur, William Mansky, Dmitri Garbuzov, Steve Zdancewic, Viktor Vafeiadis
This artifact consists of: