section ‹A simple example demonstrating parallelism for code generated towards Isabelle/ML›
theory Parallel_Example
imports Complex_Main "HOL-Library.Parallel" "HOL-Library.Debug"
begin
subsection ‹Compute-intensive examples.›
subsubsection ‹Fragments of the harmonic series›
definition harmonic :: "nat ⇒ rat" where
"harmonic n = sum_list (map (λn. 1 / of_nat n) [1..<n])"
subsubsection ‹The sieve of Erathostenes›
text ‹
The attentive reader may relate this ad-hoc implementation to the
arithmetic notion of prime numbers as a little exercise.
›
primrec mark :: "nat ⇒ nat ⇒ bool list ⇒ bool list" where
"mark _ _ [] = []"
| "mark m n (p # ps) = (case n of 0 ⇒ False # mark m m ps
| Suc n ⇒ p # mark m n ps)"
lemma length_mark [simp]:
"length (mark m n ps) = length ps"
by (induct ps arbitrary: n) (simp_all split: nat.split)
function sieve :: "nat ⇒ bool list ⇒ bool list" where
"sieve m ps = (case dropWhile Not ps
of [] ⇒ ps
| p#ps' ⇒ let n = m - length ps' in takeWhile Not ps @ p # sieve m (mark n n ps'))"
by pat_completeness auto
termination
apply (relation "measure (length ∘ snd)")
apply rule
apply (auto simp add: length_dropWhile_le)
proof -
fix ps qs q
assume "dropWhile Not ps = q # qs"
then have "length (q # qs) = length (dropWhile Not ps)" by simp
then have "length qs < length (dropWhile Not ps)" by simp
moreover have "length (dropWhile Not ps) ≤ length ps"
by (simp add: length_dropWhile_le)
ultimately show "length qs < length ps" by auto
qed
primrec natify :: "nat ⇒ bool list ⇒ nat list" where
"natify _ [] = []"
| "natify n (p#ps) = (if p then n # natify (Suc n) ps else natify (Suc n) ps)"
primrec list_primes where
"list_primes (Suc n) = natify 1 (sieve n (False # replicate n True))"
subsubsection ‹Naive factorisation›
function factorise_from :: "nat ⇒ nat ⇒ nat list" where
"factorise_from k n = (if 1 < k ∧ k ≤ n
then
let (q, r) = Divides.divmod_nat n k
in if r = 0 then k # factorise_from k q
else factorise_from (Suc k) n
else [])"
by pat_completeness auto
termination factorise_from
apply (relation "measure (λ(k, n). 2 * n - k)")
apply (auto simp add: prod_eq_iff algebra_simps elim!: dvdE)
apply (case_tac "k ≤ ka * 2")
apply (auto intro: diff_less_mono)
done
definition factorise :: "nat ⇒ nat list" where
"factorise n = factorise_from 2 n"
subsection ‹Concurrent computation via futures›
definition computation_harmonic :: "unit ⇒ rat" where
"computation_harmonic _ = Debug.timing (STR ''harmonic example'') harmonic 300"
definition computation_primes :: "unit ⇒ nat list" where
"computation_primes _ = Debug.timing (STR ''primes example'') list_primes 4000"
definition computation_future :: "unit ⇒ nat list × rat" where
"computation_future = Debug.timing (STR ''overall computation'')
(λ() ⇒ let c = Parallel.fork computation_harmonic
in (computation_primes (), Parallel.join c))"
value "computation_future ()"
definition computation_factorise :: "nat ⇒ nat list" where
"computation_factorise = Debug.timing (STR ''factorise'') factorise"
definition computation_parallel :: "unit ⇒ nat list list" where
"computation_parallel _ = Debug.timing (STR ''overall computation'')
(Parallel.map computation_factorise) [20000..<20100]"
value "computation_parallel ()"
end