[m-rev.] for review: disallow impure parallel conjuncts

[Peter Wang]

Estimated hours taken: 1.5
Branches: main

Disallow impure parallel conjuncts as they can introduce concurrency issues.
e.g. in the following X could be bound to `foo' or `bar' in different runs.

    impure set_mutvar(foo),
    (
	semipure get_mutvar(X)
    &
	impure set_mutvar(bar)
    )


compiler/purity.m:
	When computing the purity of parallel goals, add error messages
	if they are found to be semipure and impure.

tests/invalid/purity/Mmakefile:
tests/invalid/purity/impure_par_conj.err_exp:
tests/invalid/purity/impure_par_conj.m:
	Add a test case.


Index: compiler/purity.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/purity.m,v
retrieving revision 1.97
diff -u -r1.97 purity.m
--- compiler/purity.m	27 Jul 2006 05:01:22 -0000	1.97
+++ compiler/purity.m	14 Aug 2006 23:59:10 -0000
@@ -460,8 +460,15 @@
 
 compute_expr_purity(conj(ConjType, Goals0), conj(ConjType, Goals), _,
         Purity, ContainsTrace, !Info) :-
-    compute_goals_purity(Goals0, Goals, purity_pure, Purity,
-        contains_no_trace_goal, ContainsTrace, !Info).
+    (
+        ConjType = plain_conj,
+        compute_goals_purity(Goals0, Goals, purity_pure, Purity,
+            contains_no_trace_goal, ContainsTrace, !Info)
+    ;
+        ConjType = parallel_conj,
+        compute_parallel_goals_purity(Goals0, Goals, purity_pure, Purity,
+            contains_no_trace_goal, ContainsTrace, !Info)
+    ).
 compute_expr_purity(Goal0, Goal, GoalInfo, ActualPurity,
         contains_no_trace_goal, !Info) :-
     Goal0 = plain_call(PredId0, ProcId, Vars, BIState, UContext, Name0),
@@ -905,6 +912,30 @@
     !:ContainsTrace = worst_contains_trace(GoalContainsTrace, !.ContainsTrace),
     compute_cases_purity(Cases0, Cases, !Purity, !ContainsTrace, !Info).
 
+:- pred compute_parallel_goals_purity(list(hlds_goal)::in,
+    list(hlds_goal)::out, purity::in, purity::out, contains_trace_goal::in,
+    contains_trace_goal::out, purity_info::in, purity_info::out) is det.
+
+compute_parallel_goals_purity([], [], !Purity, !ContainsTrace, !Info).
+compute_parallel_goals_purity([Goal0 | Goals0], [Goal | Goals], !Purity,
+        !ContainsTrace, !Info) :-
+    compute_goal_purity(Goal0, Goal, GoalPurity, GoalContainsTrace, !Info),
+    (
+        GoalPurity = purity_pure
+    ;
+        ( GoalPurity = purity_semipure
+        ; GoalPurity = purity_impure
+        ),
+        Goal0 = _ - GoalInfo0,
+        goal_info_get_context(GoalInfo0, Context),
+        purity_info_add_message(error(impure_parallel_conjunct_error(Context,
+            GoalPurity)), !Info)
+    ),
+    !:Purity = worst_purity(GoalPurity, !.Purity),
+    !:ContainsTrace = worst_contains_trace(GoalContainsTrace, !.ContainsTrace),
+    compute_parallel_goals_purity(Goals0, Goals, !Purity, !ContainsTrace,
+        !Info).
+
 :- func worst_contains_trace(contains_trace_goal, contains_trace_goal)
     = contains_trace_goal.
 
@@ -1045,7 +1076,8 @@
     --->    missing_body_impurity_error(prog_context, pred_id)
     ;       closure_purity_error(prog_context, purity, purity)
             % closure_purity_error(Context, DeclaredPurity, ActualPurity)
-    ;       impure_unification_expr_error(prog_context, purity).
+    ;       impure_unification_expr_error(prog_context, purity)
+    ;       impure_parallel_conjunct_error(prog_context, purity).
 
 :- type post_typecheck_warning
     --->    unnecessary_body_impurity_decl(prog_context, pred_id, purity)
@@ -1065,6 +1097,9 @@
     ;
         Message = impure_unification_expr_error(Context, Purity),
         impure_unification_expr_error(Context, Purity, !IO)
+    ;
+        Message = impure_parallel_conjunct_error(Context, Purity),
+        impure_parallel_conjunct_error(Context, Purity, !IO)
     ).
 
 report_post_typecheck_message(ModuleInfo, warning(Warning), !IO) :-
@@ -1175,6 +1210,16 @@
         words("but expression was not a function call.")],
     write_error_pieces(Context, 0, Pieces, !IO).
 
+:- pred impure_parallel_conjunct_error(prog_context::in, purity::in,
+    io::di, io::uo) is det.
+
+impure_parallel_conjunct_error(Context, Purity, !IO) :-
+    purity_name(Purity, PurityName),
+    Pieces = [words("Purity error: parallel conjunct is"),
+        fixed(PurityName ++ ","),
+        words("but parallel conjuncts must be pure.")],
+    write_error_pieces(Context, 0, Pieces, !IO).
+
 %-----------------------------------------------------------------------------%
 
 :- type purity_info
Index: tests/invalid/purity/Mmakefile
===================================================================
RCS file: /home/mercury1/repository/tests/invalid/purity/Mmakefile,v
retrieving revision 1.9
diff -u -r1.9 Mmakefile
--- tests/invalid/purity/Mmakefile	21 Dec 2005 22:11:58 -0000	1.9
+++ tests/invalid/purity/Mmakefile	14 Aug 2006 23:48:15 -0000
@@ -9,6 +9,7 @@
 	impure_func_t5 \
 	impure_func_t5_fixed \
 	impure_func_t7 \
+	impure_par_conj \
 	impure_pred_t1 \
 	impure_pred_t1_fixed \
 	impure_pred_t2 \
Index: tests/invalid/purity/impure_par_conj.err_exp
===================================================================
RCS file: tests/invalid/purity/impure_par_conj.err_exp
diff -N tests/invalid/purity/impure_par_conj.err_exp
--- /dev/null	1 Jan 1970 00:00:00 -0000
+++ tests/invalid/purity/impure_par_conj.err_exp	15 Aug 2006 00:04:38 -0000
@@ -0,0 +1,8 @@
+impure_par_conj.m:014: Purity error: parallel conjunct is semipure, but
+impure_par_conj.m:014:   parallel conjuncts must be pure.
+impure_par_conj.m:018: Purity error: parallel conjunct is impure, but parallel
+impure_par_conj.m:018:   conjuncts must be pure.
+impure_par_conj.m:022: Purity error: parallel conjunct is impure, but parallel
+impure_par_conj.m:022:   conjuncts must be pure.
+impure_par_conj.m:024: Purity error: parallel conjunct is semipure, but
+impure_par_conj.m:024:   parallel conjuncts must be pure.
Index: tests/invalid/purity/impure_par_conj.m
===================================================================
RCS file: tests/invalid/purity/impure_par_conj.m
diff -N tests/invalid/purity/impure_par_conj.m
--- /dev/null	1 Jan 1970 00:00:00 -0000
+++ tests/invalid/purity/impure_par_conj.m	15 Aug 2006 00:19:42 -0000
@@ -0,0 +1,40 @@
+% We disallow impure parallel conjuncts as they can introduce concurrency
+% issues.
+
+:- module impure_par_conj.
+:- interface.
+:- import_module io.
+
+:- impure pred main(io::di, io::uo) is det.
+
+:- implementation.
+:- import_module int.
+
+main(!IO) :-
+    ( semipure get_mut(_)
+    & true
+    ),
+    ( true
+    & impure set_mut(1)
+    & true
+    ),
+    ( true
+    & impure set_mut(1)
+    & true
+    & semipure get_mut(_)
+    & true
+    ),
+    (
+	% This would be okay if the mutable was `thread_local' (which it isn't,
+	% as they're not implemented yet) or if you are absolutely certain that
+	% this mutable is only used by one thread (as in this case).
+	promise_pure
+	(
+	    semipure get_mut(X),
+	    impure set_mut(X + 1)
+	)
+    &
+	true
+    ).
+
+:- mutable(mut, int, 0, ground, [untrailed]).
--------------------------------------------------------------------------
mercury-reviews mailing list
Post messages to:       mercury-reviews at csse.unimelb.edu.au
Administrative Queries: owner-mercury-reviews at csse.unimelb.edu.au
Subscriptions:          mercury-reviews-request at csse.unimelb.edu.au
--------------------------------------------------------------------------