author  wenzelm 
Thu, 20 Dec 2007 21:12:02 +0100  
changeset 25735  4d147263f71f 
parent 25704  df9c8074ff09 
child 25775  90525e67ede7 
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 

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

5 
Dummy implementation of multithreading interface. 
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 
c661dae1070a
renamed MLSystems/multithreading_dummy.ML to MLSystems/multithreading.ML;
wenzelm
parents:
diff
changeset

21 
val self_critical: unit > bool 
c661dae1070a
renamed MLSystems/multithreading_dummy.ML to MLSystems/multithreading.ML;
wenzelm
parents:
diff
changeset

22 
datatype 'a task = 
c661dae1070a
renamed MLSystems/multithreading_dummy.ML to MLSystems/multithreading.ML;
wenzelm
parents:
diff
changeset

23 
Task of {body: unit > unit, cont: 'a > 'a, fail: 'a > 'a}  Wait  Terminate; 
c661dae1070a
renamed MLSystems/multithreading_dummy.ML to MLSystems/multithreading.ML;
wenzelm
parents:
diff
changeset

24 
val schedule: int > ('a > 'a task * 'a) > 'a > exn list 
25704  25 
val serial: unit > int 
25735  26 
val get_data: 'a Universal.tag > 'a option 
27 
val put_data: 'a Universal.tag * 'a > unit 

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); 
c661dae1070a
renamed MLSystems/multithreading_dummy.ML to MLSystems/multithreading.ML;
wenzelm
parents:
diff
changeset

40 

25735  41 

42 
(* critical section *) 

43 

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

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

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

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

47 

25735  48 

49 
(* scheduling *) 

50 

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

51 
datatype 'a task = 
c661dae1070a
renamed MLSystems/multithreading_dummy.ML to MLSystems/multithreading.ML;
wenzelm
parents:
diff
changeset

52 
Task of {body: unit > unit, cont: 'a > 'a, fail: 'a > 'a}  Wait  Terminate; 
c661dae1070a
renamed MLSystems/multithreading_dummy.ML to MLSystems/multithreading.ML;
wenzelm
parents:
diff
changeset

53 

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

54 
fun schedule _ _ _ = raise Fail "No multithreading support"; 
c661dae1070a
renamed MLSystems/multithreading_dummy.ML to MLSystems/multithreading.ML;
wenzelm
parents:
diff
changeset

55 

25735  56 

57 
(* serial numbers *) 

58 

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

61 

25735  62 

63 
(* thread data *) 

64 

65 
local 

66 

67 
val data = ref ([]: Universal.universal ref list); 

68 

69 
fun find_data tag = 

70 
let 

71 
fun find (r :: rs) = if Universal.tagIs tag (! r) then SOME r else find rs 

72 
 find [] = NONE; 

73 
in find (! data) end; 

74 

75 
in 

76 

77 
fun get_data tag = Option.map (Universal.tagProject tag o !) (find_data tag); 

78 

79 
fun put_data (tag, x) = 

80 
(case find_data tag of 

81 
SOME r => r := Universal.tagInject tag x 

82 
 NONE => data := ref (Universal.tagInject tag x) :: ! data); 

83 

84 
end; 

85 

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

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

87 

25704  88 
structure BasicMultithreading: BASIC_MULTITHREADING = Multithreading; 
89 
open BasicMultithreading; 

90 