1861 @{index_ML Exn.capture: "('a -> 'b) -> 'a -> 'b Exn.result"} \\ |
1861 @{index_ML Exn.capture: "('a -> 'b) -> 'a -> 'b Exn.result"} \\ |
1862 @{index_ML Exn.interruptible_capture: "('a -> 'b) -> 'a -> 'b Exn.result"} \\ |
1862 @{index_ML Exn.interruptible_capture: "('a -> 'b) -> 'a -> 'b Exn.result"} \\ |
1863 @{index_ML Exn.release: "'a Exn.result -> 'a"} \\ |
1863 @{index_ML Exn.release: "'a Exn.result -> 'a"} \\ |
1864 @{index_ML Par_Exn.release_all: "'a Exn.result list -> 'a list"} \\ |
1864 @{index_ML Par_Exn.release_all: "'a Exn.result list -> 'a list"} \\ |
1865 @{index_ML Par_Exn.release_first: "'a Exn.result list -> 'a list"} \\ |
1865 @{index_ML Par_Exn.release_first: "'a Exn.result list -> 'a list"} \\ |
1866 |
|
1867 \end{mldecls} |
1866 \end{mldecls} |
1868 |
1867 |
1869 \begin{description} |
1868 \begin{description} |
1870 |
1869 |
1871 \item Type @{ML_type "'a Exn.result"} represents the disjoint sum of |
1870 \item Type @{ML_type "'a Exn.result"} represents the disjoint sum of |
1901 |
1900 |
1902 \end{description} |
1901 \end{description} |
1903 *} |
1902 *} |
1904 |
1903 |
1905 |
1904 |
|
1905 subsection {* Parallel skeletons \label{sec:parlist} *} |
|
1906 |
|
1907 text {* |
|
1908 Algorithmic skeletons are combinators that operate on lists in |
|
1909 parallel, in the manner of well-known @{text map}, @{text exists}, |
|
1910 @{text forall} etc. Management of futures (\secref{sec:futures}) |
|
1911 and their results as reified exceptions is wrapped up into simple |
|
1912 programming interfaces that resemble the sequential versions. |
|
1913 |
|
1914 What remains is the application-specific problem to present |
|
1915 expressions with suitable \emph{granularity}: each list element |
|
1916 corresponds to one evaluation task. If the granularity is too |
|
1917 coarse, the available CPUs are not saturated. If it is too |
|
1918 fine-grained, CPU cycles are wasted due to the overhead of |
|
1919 organizing parallel processing. In the worst case, parallel |
|
1920 performance will be less than the sequential counterpart! |
|
1921 *} |
|
1922 |
|
1923 text %mlref {* |
|
1924 \begin{mldecls} |
|
1925 @{index_ML Par_List.map: "('a -> 'b) -> 'a list -> 'b list"} \\ |
|
1926 @{index_ML Par_List.get_some: "('a -> 'b option) -> 'a list -> 'b option"} \\ |
|
1927 \end{mldecls} |
|
1928 |
|
1929 \begin{description} |
|
1930 |
|
1931 \item @{ML Par_List.map}~@{text "f [x\<^sub>1, \<dots>, x\<^sub>n]"} is like @{ML |
|
1932 "map"}~@{text "f [x\<^sub>1, \<dots>, x\<^sub>n]"}, but the evaluation of @{text "f x\<^sub>i"} |
|
1933 for @{text "i = 1, \<dots>, n"} is performed in parallel. |
|
1934 |
|
1935 An exception in any @{text "f x\<^sub>i"} cancels the overall evaluation |
|
1936 process. The final result is produced via @{ML |
|
1937 Par_Exn.release_first} as explained above, which means the first |
|
1938 program exception that happened to occur in the parallel evaluation |
|
1939 is propagated, and all other failures are ignored. |
|
1940 |
|
1941 \item @{ML Par_List.get_some}~@{text "f [x\<^sub>1, \<dots>, x\<^sub>n]"} produces some |
|
1942 @{text "f x\<^sub>i"} that is of the form @{text "SOME y\<^sub>i"}, if that |
|
1943 exists, otherwise @{text "NONE"}. Thus it is similar to @{ML |
|
1944 Library.get_first}, but subject to a non-deterministic parallel |
|
1945 choice process. The first successful result cancels the overall |
|
1946 evaluation process; other exceptions are propagated as for @{ML |
|
1947 Par_List.map}. |
|
1948 |
|
1949 This generic parallel choice combinator is the basis for derived |
|
1950 forms, such as @{ML Par_List.find_some}, @{ML Par_List.exists}, @{ML |
|
1951 Par_List.forall}. |
|
1952 |
|
1953 \end{description} |
|
1954 *} |
|
1955 |
|
1956 text %mlex {* Subsequently, the Ackermann function is evaluated in |
|
1957 parallel for some ranges of arguments. *} |
|
1958 |
|
1959 ML_val {* |
|
1960 fun ackermann 0 n = n + 1 |
|
1961 | ackermann m 0 = ackermann (m - 1) 1 |
|
1962 | ackermann m n = ackermann (m - 1) (ackermann m (n - 1)); |
|
1963 |
|
1964 Par_List.map (ackermann 2) (500 upto 1000); |
|
1965 Par_List.map (ackermann 3) (5 upto 10); |
|
1966 *} |
|
1967 |
|
1968 |
|
1969 subsection {* Lazy evaluation *} |
|
1970 |
|
1971 text {* |
|
1972 %FIXME |
|
1973 |
|
1974 See also @{"file" "~~/src/Pure/Concurrent/lazy.ML"}. |
|
1975 *} |
|
1976 |
|
1977 |
|
1978 subsection {* Future values \label{sec:futures} *} |
|
1979 |
|
1980 text {* |
|
1981 %FIXME |
|
1982 |
|
1983 See also @{"file" "~~/src/Pure/Concurrent/future.ML"}. |
|
1984 *} |
|
1985 |
|
1986 |
1906 end |
1987 end |