+void FuncNode::set_marker(thread_id_t tid)
+{
+ marker++;
+ uint thread_id = id_to_int(tid);
+ for (uint i = thrd_marker.size(); i < thread_id + 1; i++) {
+ thrd_marker.push_back(0);
+ }
+
+ thrd_marker[thread_id] = marker;
+}
+
+/* Make sure elements of maps are initialized properly when threads enter functions */