/seL4-l4v-master/HOL4/examples/hardware/hol88/mos-count/ |
H A D | types.ml | 10 let time = ":num";; var 13 let wire = ":^time->^val";; 14 let bus = ":^time->^vec";; 16 let boolsig = ":^time->bool";; 17 let wordsig = ":^time->^word";; 18 let numsig = ":^time->num";;
|
/seL4-l4v-master/HOL4/src/metis/ |
H A D | mlibMeter.sml | 22 type limit = {time : real option, infs : int option}; 24 val unlimited = {time = NONE, infs = NONE}; 26 val expired = {time = SOME 0.0, infs = SOME 0}; 28 fun pp_limit {time,infs} = 35 add_string "time =", add_break (1,0), 36 case time of 56 type meter_reading = {time : real, infs : int}; 58 val zero_reading = {time = 0.0, infs = 0}; 60 fun add_readings {time : real, infs} {time [all...] |
H A D | mlibPortable.sml | 23 (* Pointer equality using the run-time system. *) 29 (* Timing function applications a la Mosml.time. *) 32 val time = Portable.time; value
|
H A D | mlibPortable.sig | 12 (* Pointer equality using the run-time system *) 16 val time : ('a -> 'b) -> 'a -> 'b value
|
H A D | mlibMeter.sig | 12 type limit = {time : real option, infs : int option} 19 type meter_reading = {time : real, infs : int} 25 (* mlibMeters record time and inferences *)
|
/seL4-l4v-master/seL4/include/64/mode/api/ |
H A D | ipc_buffer.h | 17 static inline word_t mode_setTimeArg(word_t i, time_t time, word_t *buffer, tcb_t *thread) argument 19 return setMR(thread, buffer, i, time);
|
/seL4-l4v-master/isabelle/src/Pure/Concurrent/ |
H A D | event_timer.scala | 4 Initiate event after given point in time. 20 final class Request private[Event_Timer](val time: Time, val repeat: Option[Time], task: TimerTask) 25 def request(time: Time, repeat: Option[Time] = None)(event: => Unit): Request = 29 case None => event_timer.schedule(task, new JDate(time.ms)) 30 case Some(rep) => event_timer.schedule(task, new JDate(time.ms), rep.ms) 32 new Request(time, repeat, task)
|
/seL4-l4v-master/l4v/isabelle/src/Pure/Concurrent/ |
H A D | event_timer.scala | 4 Initiate event after given point in time. 20 final class Request private[Event_Timer](val time: Time, val repeat: Option[Time], task: TimerTask) 25 def request(time: Time, repeat: Option[Time] = None)(event: => Unit): Request = 29 case None => event_timer.schedule(task, new JDate(time.ms)) 30 case Some(rep) => event_timer.schedule(task, new JDate(time.ms), rep.ms) 32 new Request(time, repeat, task)
|
/seL4-l4v-master/HOL4/polyml/basis/ |
H A D | Time.sml | 23 eqtype time 25 val zeroTime : time 26 val fromReal : LargeReal.real -> time 27 val toReal : time -> LargeReal.real 28 val toSeconds : time -> LargeInt.int 29 val toMilliseconds : time -> LargeInt.int 30 val toMicroseconds : time -> LargeInt.int 31 val toNanoseconds : time -> LargeInt.int 32 val fromSeconds : LargeInt.int -> time 33 val fromMilliseconds : LargeInt.int -> time 58 type time = LargeInt.int (* Becomes abstract *) type [all...] |
H A D | Timer.sml | 27 val checkCPUTimer : cpu_timer -> {usr : Time.time, sys : Time.time} 28 val checkGCTime : cpu_timer -> Time.time 31 val checkRealTimer : real_timer -> Time.time 36 nongc: { usr : Time.time, sys : Time.time}, 37 gc: { usr : Time.time, sys : Time.time} 43 type cpu_timer = {userTime: Time.time, sysTime: Time.time, gcUTim [all...] |
H A D | DATE.sig | 33 offset : Time.time option 43 val offset : date -> Time.time option 46 val localOffset : unit -> Time.time 48 val fromTimeLocal : Time.time -> date 49 val fromTimeUniv : Time.time -> date 51 val toTime : date -> Time.time
|
/seL4-l4v-master/seL4/include/32/mode/api/ |
H A D | ipc_buffer.h | 18 static inline word_t mode_setTimeArg(word_t i, time_t time, word_t *buffer, tcb_t *thread) argument 20 setMR(thread, buffer, i, (uint32_t) time); 21 return setMR(thread, buffer, i + 1, (uint32_t)(time >> 32llu));
|
/seL4-l4v-master/HOL4/src/portableML/ |
H A D | Profile.sig | 4 type call_info = {usr : Time.time, sys : Time.time, gc : Time.time, real : Time.time, n : int}
|
/seL4-l4v-master/HOL4/tools/Holmake/poly/ |
H A D | ProcessMultiplexor.sig | 19 Output of jobkey * Time.time * strmtype * string 20 | NothingSeen of jobkey * {delay: Time.time, total_elapsed : Time.time} 21 | Terminated of jobkey * exit_status * Time.time 22 | MonitorKilled of jobkey * Time.time 23 | EOF of jobkey * strmtype * Time.time
|
H A D | MB_Monitor.sig | 7 time_limit : Time.time option} ->
|
H A D | HM_Cline.sig | 11 time_limit : Time.time option,
|
/seL4-l4v-master/seL4/include/drivers/timer/ |
H A D | arm_generic.h | 19 ticks_t time; local 20 SYSTEM_READ_64(CNT_CT, time); 21 return time;
|
/seL4-l4v-master/HOL4/examples/bootstrap/ |
H A D | compiler_evalScript.sml | 21 Theorem compiler_str = time EVAL ���compiler_str���; 22 Theorem compiler_asm = time EVAL ���compiler_asm���; 23 Theorem compiler_asm_str = time EVAL ���compiler_asm_str���;
|
/seL4-l4v-master/HOL4/src/portableML/poly/ |
H A D | Multithreading.sml | 15 val sync_wait: Time.time option -> ConditionVar.conditionVar -> Mutex.mutex -> bool Exn.result 18 val tracing_time: bool -> Time.time -> (unit -> string) -> unit 64 fun sync_wait time cond lock = 68 (case time of 84 fun tracing_time detailed time = 87 else if time >= seconds 1.0 then 1 88 else if time >= seconds 0.1 then 2 89 else if time >= seconds 0.01 then 3 90 else if time >= seconds 0.001 then 4 else 5); 106 val time value [all...] |
/seL4-l4v-master/HOL4/src/portableML/poly/concurrent/ |
H A D | Timeout.sml | 9 exception TIMEOUT of Time.time 10 val apply: Time.time -> ('a -> 'b) -> 'a -> 'b 16 exception TIMEOUT of Time.time;
|
H A D | Event_Timer.sml | 4 Initiate event after given point in time. 13 val request: Time.time -> (unit -> unit) -> request 15 val future: Time.time -> unit Future.future 33 type key = Time.time 39 fun add_request time entry (requests: requests) = 40 Requests.cons_list (time, entry) requests; 59 | SOME (time, entries) => 60 if t0 < time then NONE 65 if null rest then Requests.delete time requests 66 else Requests.update (time, res [all...] |
/seL4-l4v-master/HOL4/examples/HolCheck/ |
H A D | normalFormsTest.sml | 457 val DN_valid1 = time DEF_CNF_CONV (N valid1); 458 val DNS_valid1 = time (snd o strip_exists o rhs o concl) DN_valid1; 459 val DNS_SAT_valid1 = time (HolSatLib.satOracle HolSatLib.zchaff) DNS_valid1; 466 val pigeon1 = time var_pigeon 1; (* runtime: 0.000s, gctime: 0.000s *) 467 val pigeon2 = time var_pigeon 2; (* runtime: 0.020s, gctime: 0.010s *) 468 val pigeon3 = time var_pigeon 3; (* runtime: 0.020s, gctime: 0.000s *) 469 val pigeon4 = time var_pigeon 4; (* runtime: 0.060s, gctime: 0.000s *) 470 val pigeon5 = time var_pigeon 5; (* runtime: 0.120s, gctime: 0.000s *) 471 val pigeon6 = time var_pigeon 6; (* runtime: 0.250s, gctime: 0.010s *) 472 val pigeon7 = time var_pigeo [all...] |
/seL4-l4v-master/isabelle/src/Tools/Metis/src/ |
H A D | Portable.sig | 16 (* Pointer equality using the run-time system. *) 43 val time : ('a -> 'b) -> 'a -> 'b value
|
/seL4-l4v-master/l4v/isabelle/src/Tools/Metis/src/ |
H A D | Portable.sig | 16 (* Pointer equality using the run-time system. *) 43 val time : ('a -> 'b) -> 'a -> 'b value
|
/seL4-l4v-master/HOL4/polyml/libpolyml/ |
H A D | locking.cpp | 41 #include <sys/time.h> 45 #include <time.h> 170 // Wait until a specified absolute time. Drops the lock and reaquires it. 173 void PCondVar::WaitUntil(PLock *pLock, const FILETIME *time) argument 180 liTime.HighPart = time->dwHighDateTime; 181 liTime.LowPart = time->dwLowDateTime; 182 if (liNow.QuadPart >= liTime.QuadPart) // Already past the time 189 void PCondVar::WaitUntil(PLock *pLock, const timespec *time) argument 191 pthread_cond_timedwait(&cond, &pLock->lock, time);
|