diff --git a/picus.rkt b/picus.rkt index 4823951..8f0ec36 100644 --- a/picus.rkt +++ b/picus.rkt @@ -273,16 +273,24 @@ ; | (downstream queries) ; ... (define path-sym (string-replace r1cs-path ".r1cs" ".sym")) -(define-values (res res-ks res-us readable-res-info raw-res-info) - (dpvl:apply-algorithm - r0 nwires mconstraints - input-set output-set target-set - varlist opts defs cnsts - alt-varlist alt-defs alt-cnsts - unique-set precondition ; prior knowledge row - arg-selector arg-prop arg-slv arg-timeout path-sym - solve interpret-r1cs - optimize-r1cs-p0 expand-r1cs normalize-r1cs optimize-r1cs-p1)) +(picus:log-accounting #:type "started_algorithm") +(match-define-values ((list res res-ks res-us readable-res-info raw-res-info) cpu real gc) + (time-apply (λ () + (dpvl:apply-algorithm + r0 nwires mconstraints + input-set output-set target-set + varlist opts defs cnsts + alt-varlist alt-defs alt-cnsts + unique-set precondition ; prior knowledge row + arg-selector arg-prop arg-slv arg-timeout path-sym + solve interpret-r1cs + optimize-r1cs-p0 expand-r1cs normalize-r1cs optimize-r1cs-p1)) + '())) +(picus:log-accounting #:type "finished_algorithm") +(picus:log-accounting #:type "algorithm_time" + #:value (list cpu real gc) + #:unit "(ms, ms, ms)" + #:msg "Time spent for main algorithm (cpu, real, gc)") (picus:log-debug "raw map: ~a" raw-res-info) (picus:log-debug "final unknown set ~e" res-us) (picus:log-debug "~a uniqueness: ~a" (if arg-strong "strong" "weak") res) @@ -304,6 +312,7 @@ (match res ['unsafe + (picus:log-accounting #:type "finished_with_cex") (picus:log-main "The circuit is underconstrained") (picus:log-main "Counterexample:") (match-define (list in out1 out2 other1 other2) @@ -320,8 +329,10 @@ (gen-witness raw-res-info r0))) (picus:exit exit-code:unsafe)] ['safe + (picus:log-accounting #:type "finished_with_guarantee") (picus:log-main "The circuit is properly constrained") (picus:exit exit-code:safe)] ['unknown + (picus:log-accounting #:type "finished_wo_cex") (picus:log-main "Cannot determine whether the circuit is properly constrained") (picus:exit exit-code:unknown)]))) diff --git a/picus/algorithms/dpvl.rkt b/picus/algorithms/dpvl.rkt index 4c2796b..a6d02d2 100644 --- a/picus/algorithms/dpvl.rkt +++ b/picus/algorithms/dpvl.rkt @@ -146,6 +146,10 @@ 'skip])) (values solved? (cdr res))) +(define total-cpu 0) +(define total-real 0) +(define total-gc 0) + ; select and solve ; returns: ; - (values 'normal ks us info) @@ -161,7 +165,12 @@ ; else, set not empty, move forward [else (define sid (apply-selector uspool :weight-map)) - (define-values (solved? info) (dpvl-solve ks us sid)) + (match-define-values + ((list solved? info) cpu real gc) + (time-apply (λ () (dpvl-solve ks us sid)) '())) + (set! total-cpu (+ total-cpu cpu)) + (set! total-real (+ total-real real)) + (set! total-gc (+ total-gc gc)) ; send feedback to selector (selector-feedback sid solved?) (cond @@ -351,6 +360,10 @@ ; this is required for the cex module to finalize a non-relevant part, which only requires a trivial model #:skip-query? [skip-query? #f]) + (set! total-cpu 0) + (set! total-real 0) + (set! total-gc 0) + ; first load in all global variables (set! :r0 r0) (set! :nwires nwires) @@ -487,6 +500,11 @@ ; invoke the algorithm iteration (define-values (ret0 rks rus info) (dpvl-iterate known-set unknown-set)) + (picus:log-accounting #:type "solving_time" + #:value (list total-cpu total-real total-gc) + #:unit "(ms, ms, ms)" + #:msg "Time spent for solving (cpu, real, gc)") + ; always skip x0, since it is hard-coded to 1 in the algorithm, but ; the actual value here might be different, which could be misleading. (when (hash? info) diff --git a/picus/logging.rkt b/picus/logging.rkt index 4aa4c0e..6c1a861 100644 --- a/picus/logging.rkt +++ b/picus/logging.rkt @@ -45,10 +45,13 @@ level:warning level:error level:critical + level:accounting + level:progress ;; non-standard level picus:log-main picus:log-progress + (rename-out [picus:log-accounting* picus:log-accounting]) define/caller) @@ -159,10 +162,14 @@ (define-picus-level error 40) (define-picus-level critical 50) -;; custom level: progress -(define-picus-level progress 15) +;; custom levels +;; note that in SaaS, accounting has level 25 and progress has level 26 +;; but for standalone application, both levels are very noisy, +;; so we set them below the info level (20). +(define-picus-level accounting 15) +(define-picus-level progress 16) -;; from https://docs.python.org/3/library/logging.html#logging-levels +;; Mostly from https://docs.python.org/3/library/logging.html#logging-levels (define-log-function debug) (define-log-function info) (define-log-function warning) @@ -173,6 +180,20 @@ (define-log-function main #:picus info #:rkt info) ;; This is for the algorithm progress. (define-log-function progress #:rkt debug) +;; Accounting +(define-log-function accounting #:rkt debug) + +(define/caller (picus:log-accounting* #:type entry-type + #:unit [entry-unit "unit"] + #:value [entry-value 1] + #:msg [msg ""]) + #:caller caller + + (picus:log-accounting "~a" msg + #:extra (hash 'accounting (hash 'entry_type entry-type + 'entry_unit entry-unit + 'entry_value entry-value) + 'caller caller))) (define/caller (picus:log-exception e) #:caller caller - (picus:log-error "~e" (exn->string e) #:extra (hash 'caller caller))) + (picus:log-error "exception: ~e" (exn->string e) #:extra (hash 'caller caller)))