kind of tired

songyahui · May 9, 2024 · 6865f0c · 6865f0c
1 parent 4131d8b
commit 6865f0c
Show file tree

Hide file tree

Showing 2 changed files with 18 additions and 19 deletions.
diff --git a/parsing/hiplib.ml b/parsing/hiplib.ml
@@ -723,7 +723,7 @@ let normal_report ?(kind="Function") ?given_spec ?given_spec_n ?inferred_spec ?i
     | None -> "") ^
     normed_spec ^
     (match inferred_spec with
-    | Some _ (* s *) -> "[Raw Post Spec] OMITTED\n" (*^ string_of_spec_list s ^ "\n\n" *)
+    | Some _  (* s *) -> "" (*"[Raw Post Spec] OMITTED\n" ^ string_of_spec_list s ^ "\n\n" *)
     | None -> "") ^
     normed_post ^
     (match forward_time_ms with

diff --git a/src/demo/8_schduler.ml b/src/demo/8_schduler.ml
@@ -29,7 +29,7 @@ let queue_create () = ref ([], [])
 
 let queue_push ele queue 
 (*@
-ex m m' q q'; req queue->q /\ effNo(q) = m /\ m>=0; 
+ex m m' q q' w; req queue->q /\ effNo(q) = m /\ m>=0; 
 ens  queue->q' /\ effNo(q') = m' /\ m'>0 /\ effNo(ele)=w /\ w >0 /\ m'=m+w /\ res=() 
 @*)
 = let (front, back) = !queue in
@@ -85,7 +85,7 @@ ens  run_q->q' /\ effNo(q') = m' /\ m'>=0  /\ effNo(f) =w /\ w >0 /\ m'+w=m /\
   Norm(non_empty_queue(queue, mm') /\ effNo(ele)=w /\ w >0 /\ mm'=mm+w /\ res=inter /\ inter=()) *)
 let enqueue ele queue
 (*@
-ex m m' q q'; req queue->q /\ effNo(q) = m /\ m>=0; 
+ex m m' q q' w; req queue->q /\ effNo(q) = m /\ m>=0; 
 ens  queue->q' /\ effNo(q') = m' /\ m'>0 /\ effNo(ele)=w /\ w >0 /\ m'=m+w /\ res=() 
 @*)
 = queue_push ele queue
@@ -114,21 +114,12 @@ ex cr; spawn (f, run_q, cr)
 
 (*@ predicate task(f) = 
      Norm(effNo(f) = 0 /\ res=())
-  \/ ex n r1 f2; ens effNo(f)=n/\n>0/\effNo(f2)=n-1; Yield(emp, r1); task(f2)
-  \/ ex r r1 f1 f2 r2 n m1 m2; 
-     ens effNo(f)=n /\ n>0 /\ effNo(f1)= m1 /\ effNo(f2)=m2 /\ m1>0 /\ m2>0 /\ (m1+m2)=(n-1); 
-     Fork(emp, f1, r1); task(f2) 
-@*)  
+  \/ ex n r1; ens effNo(f)=n/\n>0/\effNo(k)=n-1; Yield(emp, r1)
+  \/ ex r1 f1 n m1 m2; 
+     ens effNo(f)=n /\ n>0 /\ effNo(f1)= m1 /\ effNo(k)=m2 /\ m1>0 /\ m2>0 /\ (m1+m2)=(n-1); 
+     Fork(emp, f1, r1)
+@*) 
 
-(*
- ex r; queue_is_empty(run_q, true) ; ens effNo(f)=0 /\ res =r /\ r= () 
-\/ ex m m' w w' ele cr; req non_empty_queue(run_q, m);  
-   Norm(any_queue(run_q, m') /\ effNo(f)=0 /\ effNo(ele) =w' /\ m'<m );
-   spawn (ele, run_q, cr); Norm(res=cr)
-\/ ex m m' w w' ele cr qq mm; req any_queue(run_q, m) /\ effNo(qq)=mm /\ mm>0 ;  
-    Norm(any_queue(run_q, m') /\ effNo(f)=w /\ effNo(ele) =w' /\ w>0 /\ w'>0 /\ (w'+m')<(m+w) );
-    spawn (ele, run_q, cr); Norm(res=cr)
-*)
 let rec spawn f run_q 
 (*@
    ex q; req run_q->q /\ effNo(q)=0 /\ effNo(f)=0; ens run_q->q  /\ res=() 
@@ -139,18 +130,26 @@ let rec spawn f run_q
    req run_q->q /\effNo(q)=m/\m>=0; ens run_q->q' /\effNo(q')=m'/\m'>=0  
    /\ effNo(f)=w /\ effNo(ele) =w' /\ w>0 /\ w'>0 /\ (w'+m')<(m+w) ;
    spawn (ele, run_q, cr)
-@*) 
+@*)  
 = match (*f ()*) task(f) with
   (* spawn (f, run_q, res) *)
   | x -> dequeue run_q;
   | effect Yield k ->
      enqueue k run_q;
-     dequeue run_q
+     dequeue run_q 
   | effect (Fork f') k -> 
      enqueue k run_q; 
      spawn f' run_q
 
 
+(* ex r; queue_is_empty(run_q, true) ; ens effNo(f)=0 /\ res =r /\ r= () 
+\/ ex m m' w w' ele cr; req non_empty_queue(run_q, m);  
+   Norm(any_queue(run_q, m') /\ effNo(f)=0 /\ effNo(ele) =w' /\ m'<m );
+   spawn (ele, run_q, cr); Norm(res=cr)
+\/ ex m m' w w' ele cr qq mm; req any_queue(run_q, m) /\ effNo(qq)=mm /\ mm>0 ;  
+    Norm(any_queue(run_q, m') /\ effNo(f)=w /\ effNo(ele) =w' /\ w>0 /\ w'>0 /\ (w'+m')<(m+w) );
+    spawn (ele, run_q, cr); Norm(res=cr)
+*)
 (*
 (* A concurrent round-robin scheduler *)
 let run main