#include <upc.h>
#include <stddef.h>
int main() {
  int x = upc_threadof(NULL);
}