jeehoonkang

#include <stdio.h>
#include <stdlib.h>

int main() {
  char *p = malloc(0x80000000);
  *((char *)0x80000000) = 3;
  return 0;
}

// test with: gcc -S -O2 tt.c && cat tt.s

jeehoonkang

A Formal C Memory Model Supporting Integer-Pointer Casts

Jeehoon Kang, Chung-Kil Hur, William Mansky, Dmitri Garbuzov, Steve Zdancewic, Viktor Vafeiadis

This artifact consists of:

• example C source codes presented in the paper; and
• Coq formalization for our memory model and verification of example transformations.

Virtual Machine

jeehoonkang

Midterm Exam Announcement

• Software Lab, 3rd floor, Bldg 302
• 1700-1830 20150430 (Thu)
• Those who want to bring their own notebooks?

I am busy these days...

• Sorry for late response these days.
• I will keep you updated as deliberately as possible.

Proof Example

jeehoonkang

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.
 **)

jeehoonkang

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

jeehoonkang

Lightweight Verification of Separate Compilation

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".

jeehoonkang

#include <cstdio>

using namespace std;

int main() {
  setbuf(stdout, NULL);

  int nCase;
  scanf("%d", &nCase);

jeehoonkang

./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))

jeehoonkang

(** **** 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.

jeehoonkang

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.

Series of Optimizations

• By some global analysis, deduce that r2 should be 0 or 1. Thus transform thread 2 into:

  r2 = y;
  if (r2) {
    x = 1
  } else {