|
1 header {* A simple example demonstrating parallelism for code generated towards Isabelle/ML *} |
|
2 |
|
3 theory Parallel_Example |
|
4 imports Complex_Main "~~/src/HOL/Library/Parallel" "~~/src/HOL/Library/Debug" |
|
5 begin |
|
6 |
|
7 subsection {* Compute-intensive examples. *} |
|
8 |
|
9 subsubsection {* Fragments of the harmonic series *} |
|
10 |
|
11 definition harmonic :: "nat \<Rightarrow> rat" where |
|
12 "harmonic n = listsum (map (\<lambda>n. 1 / of_nat n) [1..<n])" |
|
13 |
|
14 |
|
15 subsubsection {* The sieve of Erathostenes *} |
|
16 |
|
17 text {* |
|
18 The attentive reader may relate this ad-hoc implementation to the |
|
19 arithmetic notion of prime numbers as a little exercise. |
|
20 *} |
|
21 |
|
22 primrec mark :: "nat \<Rightarrow> nat \<Rightarrow> bool list \<Rightarrow> bool list" where |
|
23 "mark _ _ [] = []" |
|
24 | "mark m n (p # ps) = (case n of 0 \<Rightarrow> False # mark m m ps |
|
25 | Suc n \<Rightarrow> p # mark m n ps)" |
|
26 |
|
27 lemma length_mark [simp]: |
|
28 "length (mark m n ps) = length ps" |
|
29 by (induct ps arbitrary: n) (simp_all split: nat.split) |
|
30 |
|
31 function sieve :: "nat \<Rightarrow> bool list \<Rightarrow> bool list" where |
|
32 "sieve m ps = (case dropWhile Not ps |
|
33 of [] \<Rightarrow> ps |
|
34 | p#ps' \<Rightarrow> let n = m - length ps' in takeWhile Not ps @ p # sieve m (mark n n ps'))" |
|
35 by pat_completeness auto |
|
36 |
|
37 termination -- {* tuning of this proof is left as an exercise to the reader *} |
|
38 apply (relation "measure (length \<circ> snd)") |
|
39 apply rule |
|
40 apply (auto simp add: length_dropWhile_le) |
|
41 proof - |
|
42 fix ps qs q |
|
43 assume "dropWhile Not ps = q # qs" |
|
44 then have "length (q # qs) = length (dropWhile Not ps)" by simp |
|
45 then have "length qs < length (dropWhile Not ps)" by simp |
|
46 moreover have "length (dropWhile Not ps) \<le> length ps" |
|
47 by (simp add: length_dropWhile_le) |
|
48 ultimately show "length qs < length ps" by auto |
|
49 qed |
|
50 |
|
51 primrec natify :: "nat \<Rightarrow> bool list \<Rightarrow> nat list" where |
|
52 "natify _ [] = []" |
|
53 | "natify n (p#ps) = (if p then n # natify (Suc n) ps else natify (Suc n) ps)" |
|
54 |
|
55 primrec list_primes where |
|
56 "list_primes (Suc n) = natify 1 (sieve n (False # replicate n True))" |
|
57 |
|
58 |
|
59 subsubsection {* Naive factorisation *} |
|
60 |
|
61 function factorise_from :: "nat \<Rightarrow> nat \<Rightarrow> nat list" where |
|
62 "factorise_from k n = (if 1 < k \<and> k \<le> n |
|
63 then |
|
64 let (q, r) = divmod_nat n k |
|
65 in if r = 0 then k # factorise_from k q |
|
66 else factorise_from (Suc k) n |
|
67 else [])" |
|
68 by pat_completeness auto |
|
69 |
|
70 termination factorise_from -- {* tuning of this proof is left as an exercise to the reader *} |
|
71 term measure |
|
72 apply (relation "measure (\<lambda>(k, n). 2 * n - k)") |
|
73 apply (auto simp add: prod_eq_iff) |
|
74 apply (case_tac "k \<le> 2 * q") |
|
75 apply (rule diff_less_mono) |
|
76 apply auto |
|
77 done |
|
78 |
|
79 definition factorise :: "nat \<Rightarrow> nat list" where |
|
80 "factorise n = factorise_from 2 n" |
|
81 |
|
82 |
|
83 subsection {* Concurrent computation via futures *} |
|
84 |
|
85 definition computation_harmonic :: "unit \<Rightarrow> rat" where |
|
86 "computation_harmonic _ = Debug.timing (STR ''harmonic example'') harmonic 300" |
|
87 |
|
88 definition computation_primes :: "unit \<Rightarrow> nat list" where |
|
89 "computation_primes _ = Debug.timing (STR ''primes example'') list_primes 4000" |
|
90 |
|
91 definition computation_future :: "unit \<Rightarrow> nat list \<times> rat" where |
|
92 "computation_future = Debug.timing (STR ''overall computation'') |
|
93 (\<lambda>() \<Rightarrow> let c = Parallel.fork computation_harmonic |
|
94 in (computation_primes (), Parallel.join c))" |
|
95 |
|
96 value [code] "computation_future ()" |
|
97 |
|
98 definition computation_factorise :: "nat \<Rightarrow> nat list" where |
|
99 "computation_factorise = Debug.timing (STR ''factorise'') factorise" |
|
100 |
|
101 definition computation_parallel :: "unit \<Rightarrow> nat list list" where |
|
102 "computation_parallel _ = Debug.timing (STR ''overall computation'') |
|
103 (Parallel.map computation_factorise) [20000..<20100]" |
|
104 |
|
105 value [code] "computation_parallel ()" |
|
106 |
|
107 end |
|
108 |