#include "common.h"

__attribute__ ((aligned (16))) char stack0[4096 * NCPU];

void start() {

}