Dispatch Queue VCC Update (#714)

Author: xiazhvera

.github/workflows/proof-alarm.yml

@@ -16,7 +16,7 @@ jobs:
     - name: Check
       run: |
         TMPFILE=$(mktemp)
-        echo "111d190288082ce7cebe929719747267 source/linux/epoll_event_loop.c" > $TMPFILE
+        echo "e857a2e5f72ab77a94e56372d89abf99 source/linux/epoll_event_loop.c" > $TMPFILE
         md5sum --check $TMPFILE
 
     # No further steps if successful

tests/vcc/Makefile

@@ -22,9 +22,9 @@ NO_CHANGE_FILE=source/linux/epoll_event_loop.c
 	$(VCC) $(VCC_ARGS) process_task_pre_queue.c /f:s_process_task_pre_queue
 	$(VCC) $(VCC_ARGS) lifecycle.c /f:s_stop_task /f:s_stop /f:s_wait_for_stop_completion /f:s_run
 	$(VCC) $(VCC_ARGS) main_loop.c /f:s_on_tasks_to_schedule /f:s_main_loop
-	$(VCC) $(VCC_ARGS) new_destroy.c /f:aws_event_loop_new_default
-	$(VCC) $(VCC_ARGS) new_destroy.c /f:aws_event_loop_new_with_epoll /f:s_destroy /p:"-DUSE_EFD=0"
-	$(VCC) $(VCC_ARGS) new_destroy.c /f:aws_event_loop_new_with_epoll /f:s_destroy /p:"-DUSE_EFD=1"
+	$(VCC) $(VCC_ARGS) new_destroy.c /f:aws_event_loop_new_default /f:s_start_destroy
+	$(VCC) $(VCC_ARGS) new_destroy.c /f:aws_event_loop_new_with_epoll /f:s_complete_destroy /p:"-DUSE_EFD=0"
+	$(VCC) $(VCC_ARGS) new_destroy.c /f:aws_event_loop_new_with_epoll /f:s_complete_destroy /p:"-DUSE_EFD=1"
 	$(VCC) $(VCC_ARGS) client.c /f:test_new_destroy /f:test_subscribe_unsubscribe
 
 .phony: all

tests/vcc/client.c

@@ -37,7 +37,8 @@ void test_new_destroy()
     if (!event_loop) return;
     _(ghost \claim c_event_loop;)
     _(ghost c_event_loop = \make_claim({event_loop}, event_loop->\closed);)
-    s_destroy(event_loop _(ghost c_event_loop) _(ghost c_mutex));
+    s_start_destroy(event_loop _(ghost c_event_loop) _(ghost c_mutex));
+    s_complete_destroy(event_loop _(ghost c_event_loop) _(ghost c_mutex));
 }
 
 void on_event(

tests/vcc/new_destroy.c

@@ -249,11 +249,17 @@ struct aws_event_loop *aws_event_loop_new_with_epoll(
     return NULL;
 }
 
+static void s_start_destroy(struct aws_event_loop *event_loop
+    _(ghost \claim(c_event_loop)) _(ghost \claim(c_mutex))
+) {
+    (void)event_loop;
+}
+
 /* Fake-up call to s_stop since this is just a vtable lookup */
 #define aws_event_loop_stop(event_loop) \
     s_stop(event_loop _(ghost c_event_loop) _(ghost c_mutex));
 
-static void s_destroy(struct aws_event_loop *event_loop
+static void s_complete_destroy(struct aws_event_loop *event_loop
     _(ghost \claim(c_event_loop)) _(ghost \claim(c_mutex))
 ) {
     AWS_LOGF_INFO(AWS_LS_IO_EVENT_LOOP, "id=%p: Destroying event_loop", (void *)event_loop);

tests/vcc/preamble.h

@@ -827,7 +827,20 @@ struct aws_event_loop *aws_event_loop_new_with_epoll(
         \fresh(c_mutex) && \wrapped0(c_mutex) && \claims_object(c_mutex, &(epoll_loop_of(\result)->task_pre_queue_mutex))))
 ;
 
-static void s_destroy(struct aws_event_loop *event_loop
+static void s_start_destroy(struct aws_event_loop *event_loop
+    _(ghost \claim(c_event_loop)) _(ghost \claim(c_mutex))
+)
+    _(requires \malloc_root(event_loop))
+    _(requires \malloc_root(epoll_loop_of(event_loop)))
+    _(requires c_event_loop != c_mutex)
+    _(requires \wrapped0(c_event_loop) && \claims_object(c_event_loop, event_loop))
+    _(requires \wrapped0(c_mutex) && \claims_object(c_mutex, &epoll_loop_of(event_loop)->task_pre_queue_mutex))
+    _(requires \wrapped(&epoll_loop_of(event_loop)->scheduler))
+    _(requires \wrapped(epoll_loop_of(event_loop)::status))
+    _(requires \wrapped(&epoll_loop_of(event_loop)->stop_task))
+;
+
+static void s_complete_destroy(struct aws_event_loop *event_loop
     _(ghost \claim(c_event_loop)) _(ghost \claim(c_mutex))
 )
     _(requires \malloc_root(event_loop))