author  wenzelm 
Tue, 09 Sep 2008 23:48:36 +0200  
changeset 28187  4062882c7df3 
parent 28169  356fc8734741 
child 28460  455ef74607d7 
permissions  rwrr 
24690
c661dae1070a
renamed MLSystems/multithreading_dummy.ML to MLSystems/multithreading.ML;
wenzelm
parents:
diff
changeset

1 
(* Title: Pure/MLSystems/multithreading.ML 
c661dae1070a
renamed MLSystems/multithreading_dummy.ML to MLSystems/multithreading.ML;
wenzelm
parents:
diff
changeset

2 
ID: $Id$ 
c661dae1070a
renamed MLSystems/multithreading_dummy.ML to MLSystems/multithreading.ML;
wenzelm
parents:
diff
changeset

3 
Author: Makarius 
c661dae1070a
renamed MLSystems/multithreading_dummy.ML to MLSystems/multithreading.ML;
wenzelm
parents:
diff
changeset

4 

28149  5 
Dummy implementation of multithreading setup. 
24690
c661dae1070a
renamed MLSystems/multithreading_dummy.ML to MLSystems/multithreading.ML;
wenzelm
parents:
diff
changeset

6 
*) 
c661dae1070a
renamed MLSystems/multithreading_dummy.ML to MLSystems/multithreading.ML;
wenzelm
parents:
diff
changeset

7 

25704  8 
signature BASIC_MULTITHREADING = 
9 
sig 

10 
val NAMED_CRITICAL: string > (unit > 'a) > 'a 

11 
val CRITICAL: (unit > 'a) > 'a 

12 
end; 

13 

24690
c661dae1070a
renamed MLSystems/multithreading_dummy.ML to MLSystems/multithreading.ML;
wenzelm
parents:
diff
changeset

14 
signature MULTITHREADING = 
c661dae1070a
renamed MLSystems/multithreading_dummy.ML to MLSystems/multithreading.ML;
wenzelm
parents:
diff
changeset

15 
sig 
25704  16 
include BASIC_MULTITHREADING 
24690
c661dae1070a
renamed MLSystems/multithreading_dummy.ML to MLSystems/multithreading.ML;
wenzelm
parents:
diff
changeset

17 
val trace: int ref 
c661dae1070a
renamed MLSystems/multithreading_dummy.ML to MLSystems/multithreading.ML;
wenzelm
parents:
diff
changeset

18 
val tracing: int > (unit > string) > unit 
c661dae1070a
renamed MLSystems/multithreading_dummy.ML to MLSystems/multithreading.ML;
wenzelm
parents:
diff
changeset

19 
val available: bool 
c661dae1070a
renamed MLSystems/multithreading_dummy.ML to MLSystems/multithreading.ML;
wenzelm
parents:
diff
changeset

20 
val max_threads: int ref 
25775
90525e67ede7
added Multithreading.max_threads_value, which maps a value of 0 to number of CPUs;
wenzelm
parents:
25735
diff
changeset

21 
val max_threads_value: unit > int 
28149  22 
val no_interrupts: Thread.threadAttribute list 
28160  23 
val regular_interrupts: Thread.threadAttribute list 
24 
val with_attributes: Thread.threadAttribute list > 

25 
(Thread.threadAttribute list > 'a > 'b) > 'a > 'b 

24690
c661dae1070a
renamed MLSystems/multithreading_dummy.ML to MLSystems/multithreading.ML;
wenzelm
parents:
diff
changeset

26 
val self_critical: unit > bool 
25704  27 
val serial: unit > int 
24690
c661dae1070a
renamed MLSystems/multithreading_dummy.ML to MLSystems/multithreading.ML;
wenzelm
parents:
diff
changeset

28 
end; 
c661dae1070a
renamed MLSystems/multithreading_dummy.ML to MLSystems/multithreading.ML;
wenzelm
parents:
diff
changeset

29 

c661dae1070a
renamed MLSystems/multithreading_dummy.ML to MLSystems/multithreading.ML;
wenzelm
parents:
diff
changeset

30 
structure Multithreading: MULTITHREADING = 
c661dae1070a
renamed MLSystems/multithreading_dummy.ML to MLSystems/multithreading.ML;
wenzelm
parents:
diff
changeset

31 
struct 
c661dae1070a
renamed MLSystems/multithreading_dummy.ML to MLSystems/multithreading.ML;
wenzelm
parents:
diff
changeset

32 

25735  33 
(* options *) 
34 

24690
c661dae1070a
renamed MLSystems/multithreading_dummy.ML to MLSystems/multithreading.ML;
wenzelm
parents:
diff
changeset

35 
val trace = ref (0: int); 
c661dae1070a
renamed MLSystems/multithreading_dummy.ML to MLSystems/multithreading.ML;
wenzelm
parents:
diff
changeset

36 
fun tracing _ _ = (); 
c661dae1070a
renamed MLSystems/multithreading_dummy.ML to MLSystems/multithreading.ML;
wenzelm
parents:
diff
changeset

37 

c661dae1070a
renamed MLSystems/multithreading_dummy.ML to MLSystems/multithreading.ML;
wenzelm
parents:
diff
changeset

38 
val available = false; 
c661dae1070a
renamed MLSystems/multithreading_dummy.ML to MLSystems/multithreading.ML;
wenzelm
parents:
diff
changeset

39 
val max_threads = ref (1: int); 
25775
90525e67ede7
added Multithreading.max_threads_value, which maps a value of 0 to number of CPUs;
wenzelm
parents:
25735
diff
changeset

40 
fun max_threads_value () = Int.max (! max_threads, 1); 
24690
c661dae1070a
renamed MLSystems/multithreading_dummy.ML to MLSystems/multithreading.ML;
wenzelm
parents:
diff
changeset

41 

28187
4062882c7df3
proper values of no_interrupts, regular_interrupts;
wenzelm
parents:
28169
diff
changeset

42 
val no_interrupts = 
4062882c7df3
proper values of no_interrupts, regular_interrupts;
wenzelm
parents:
28169
diff
changeset

43 
[Thread.EnableBroadcastInterrupt false, Thread.InterruptState Thread.InterruptDefer]; 
4062882c7df3
proper values of no_interrupts, regular_interrupts;
wenzelm
parents:
28169
diff
changeset

44 

4062882c7df3
proper values of no_interrupts, regular_interrupts;
wenzelm
parents:
28169
diff
changeset

45 
val regular_interrupts = 
4062882c7df3
proper values of no_interrupts, regular_interrupts;
wenzelm
parents:
28169
diff
changeset

46 
[Thread.EnableBroadcastInterrupt true, Thread.InterruptState Thread.InterruptAsynchOnce]; 
28160  47 

48 
fun with_attributes _ f x = f [] x; 

28149  49 

25735  50 

51 
(* critical section *) 

52 

24690
c661dae1070a
renamed MLSystems/multithreading_dummy.ML to MLSystems/multithreading.ML;
wenzelm
parents:
diff
changeset

53 
fun self_critical () = false; 
c661dae1070a
renamed MLSystems/multithreading_dummy.ML to MLSystems/multithreading.ML;
wenzelm
parents:
diff
changeset

54 
fun NAMED_CRITICAL _ e = e (); 
c661dae1070a
renamed MLSystems/multithreading_dummy.ML to MLSystems/multithreading.ML;
wenzelm
parents:
diff
changeset

55 
fun CRITICAL e = e (); 
c661dae1070a
renamed MLSystems/multithreading_dummy.ML to MLSystems/multithreading.ML;
wenzelm
parents:
diff
changeset

56 

25735  57 

58 
(* serial numbers *) 

59 

25704  60 
local val count = ref (0: int) 
61 
in fun serial () = (count := ! count + 1; ! count) end; 

62 

28123
53cd972d7db9
provide dummy thread structures, including proper Thread.getLocal/setLocal;
wenzelm
parents:
26082
diff
changeset

63 
end; 
53cd972d7db9
provide dummy thread structures, including proper Thread.getLocal/setLocal;
wenzelm
parents:
26082
diff
changeset

64 

53cd972d7db9
provide dummy thread structures, including proper Thread.getLocal/setLocal;
wenzelm
parents:
26082
diff
changeset

65 
structure BasicMultithreading: BASIC_MULTITHREADING = Multithreading; 
53cd972d7db9
provide dummy thread structures, including proper Thread.getLocal/setLocal;
wenzelm
parents:
26082
diff
changeset

66 
open BasicMultithreading; 