[m-rev.] for review: atomic scope fixes
Peter Wang
novalazy at gmail.com
Thu Nov 5 16:55:14 AEDT 2009
Branches: main
Fix some problems with `atomic' scopes. In particular, state variables in
atomic scopes now works (again?)
compiler/hlds_goal.m:
compiler/saved_vars.m:
Add a goal feature to indicate when a goal within an atomic scope has
stm_from_outer_to_inner/stm_from_inner_to_outer calls added.
compiler/quantification.m:
Add a predicate to quantify goals inside an atomic scope.
Quantification may occur before the calls to stm_from_*_to_* are
inserted. If that is not taken into account, the nonlocal set for
an atomic goal won't include its inner interface variables, causing
problems (e.g. variables being renamed away).
Don't explicitly delete inner variables from the nonlocal vars of
atomic scope; this has no effect. [Also, it only deleted the inner
variables for the main atomic goal. The inner variables of the or_else
goals probably needed to be deleted as well.]
compiler/purity.m:
Remove code that checks STM inner variables are not used outside of the
atomic scope, and outer variables not used within. The changes in
quantification.m broke the assumption that inner variables don't appear
in the nonlocals of their respective atomic goals. Mode checking
should catch the same errors anyway.
Add the new goal feature after inserting stm_from_*_to_* calls.
compiler/state_var.m:
In svar_start_inner_atomic_scope, return the "dot" variable as inner
`di' variable. Before, it returned the "colon" variable which resulted
in an incorrect ordering in the expanded goal.
In svar_finish_inner_atomic_scope, use the "dot" variable as the
inner `uo' variable.
compiler/typecheck.m:
Unify the types of the outer variables on an atomic scope.
tests/stm/Mmakefile:
tests/stm/atomic_conj.exp:
tests/stm/atomic_conj.m:
tests/stm/atomic_ite.exp:
tests/stm/atomic_ite.m:
Add test cases.
diff --git a/compiler/hlds_goal.m b/compiler/hlds_goal.m
index d5ff791..a6f29a3 100644
--- a/compiler/hlds_goal.m
+++ b/compiler/hlds_goal.m
@@ -1470,13 +1470,17 @@
% pretest-equality if-then-else goal. The goal feature is required
% to allow pointer comparisons generated by the compiler.
- ; feature_lambda_undetermined_mode.
+ ; feature_lambda_undetermined_mode
% This goal is a lambda goal converted from a higher order term
% for which we don't know the mode of the call to the underlying
% predicate. These can be produced by the polymorphism
% transformation but should be removed by the end of mode
% checking.
+ ; feature_contains_stm_inner_outer.
+ % This goal is a goal inside an atomic scope, for which the calls
+ % to convert inner and outer variables have been inserted.
+
%-----------------------------------------------------------------------------%
%
% The rename_var* predicates take a structure and a mapping from var -> var
diff --git a/compiler/purity.m b/compiler/purity.m
index 2fd65ad..76baad6 100644
--- a/compiler/purity.m
+++ b/compiler/purity.m
@@ -784,58 +784,16 @@ compute_expr_purity(GoalExpr0, GoalExpr, GoalInfo, Purity, ContainsTrace,
purity_info::in, purity_info::out) is det.
wrap_inner_outer_goals(Outer, Goal0 - Inner, Goal, !Info) :-
- % Generate an error if the outer variables are in the nonlocals of the
- % original goal, since they are not supposed to be used in the goal.
- %
- % Generate an error if the inner variables are in the nonlocals of the
- % original goal, since they are not supposed to be used outside the goal.
Goal0 = hlds_goal(_, GoalInfo0),
NonLocals0 = goal_info_get_nonlocals(GoalInfo0),
Context = goal_info_get_context(GoalInfo0),
Outer = atomic_interface_vars(OuterDI, OuterUO),
Inner = atomic_interface_vars(InnerDI, InnerUO),
- list.filter(set.contains(NonLocals0), [OuterUO, OuterDI], PresentOuter),
- list.filter(set.contains(NonLocals0), [InnerUO, InnerDI], PresentInner),
- VarSet = !.Info ^ pi_varset,
- (
- PresentOuter = []
- ;
- PresentOuter = [_ | _],
- PresentOuterVarNames =
- list.map(mercury_var_to_string(VarSet, no), PresentOuter),
- Pieces1 = [words("Outer"),
- words(choose_number(PresentOuterVarNames,
- "variable", "variables"))] ++
- list_to_pieces(PresentOuterVarNames) ++
- [words(choose_number(PresentOuterVarNames, "is", "are")),
- words("present in the atomic goal.")],
- Msg1 = error_msg(yes(Context), do_not_treat_as_first, 0,
- [always(Pieces1)]),
- Spec1 = error_spec(severity_error, phase_type_check, [Msg1]),
- purity_info_add_message(Spec1, !Info)
- ),
- (
- PresentInner = []
- ;
- PresentInner = [_ | _],
- PresentInnerVarNames =
- list.map(mercury_var_to_string(VarSet, no), PresentInner),
- Pieces2 = [words("Inner"),
- words(choose_number(PresentInnerVarNames,
- "variable", "variables"))] ++
- list_to_pieces(PresentInnerVarNames) ++
- [words(choose_number(PresentInnerVarNames, "is", "are")),
- words("present outside the atomic goal.")],
- Msg2 = error_msg(yes(Context), do_not_treat_as_first, 0,
- [always(Pieces2)]),
- Spec2 = error_spec(severity_error, phase_type_check, [Msg2]),
- purity_info_add_message(Spec2, !Info)
- ),
- % generate the outer_to_inner and inner_to_outer goals
+ % Generate the STM outer_to_inner and inner_to_outer goals.
OuterToInnerPred = "stm_from_outer_to_inner",
InnerToOuterPred = "stm_from_inner_to_outer",
- ModuleInfo = !.Info^pi_module_info,
+ ModuleInfo = !.Info ^ pi_module_info,
generate_simple_call(mercury_stm_builtin_module,
OuterToInnerPred, pf_predicate, only_mode,
detism_det, purity_pure, [OuterDI, InnerDI], [],
@@ -855,7 +813,9 @@ wrap_inner_outer_goals(Outer, Goal0 - Inner, Goal, !Info) :-
% goal, and *should* be used by code outside the goal. However, even if
% they are not, the nonlocals set is allowed to overapproximate.
set.insert_list(NonLocals0, [OuterDI, OuterUO], NonLocals),
- goal_info_set_nonlocals(NonLocals, GoalInfo0, GoalInfo),
+ goal_info_set_nonlocals(NonLocals, GoalInfo0, GoalInfo1),
+ goal_info_add_feature(feature_contains_stm_inner_outer, GoalInfo1,
+ GoalInfo),
Goal = hlds_goal(WrapExpr, GoalInfo).
:- pred check_outer_var_type(prog_context::in, vartypes::in, prog_varset::in,
diff --git a/compiler/quantification.m b/compiler/quantification.m
index 1a13763..8e188b7 100644
--- a/compiler/quantification.m
+++ b/compiler/quantification.m
@@ -107,6 +107,7 @@
:- import_module hlds.instmap.
:- import_module libs.compiler_util.
+:- import_module assoc_list.
:- import_module bool.
:- import_module map.
:- import_module maybe.
@@ -568,6 +569,7 @@ implicitly_quantify_goal_quant_info_2(GoalExpr0, GoalExpr, GoalInfo0,
(
ShortHand0 = atomic_goal(GoalType, Outer, Inner, MaybeOutputVars,
MainGoal0, OrElseGoals0, OrElseInners0),
+
% The call to implicitly_quantify_disj causes the inner STM
% interface variables to be renamed in any or_else goals, but
% doing it first explicitly allows the new names of these
@@ -582,11 +584,14 @@ implicitly_quantify_goal_quant_info_2(GoalExpr0, GoalExpr, GoalInfo0,
OrElseGoals1 = OrElseGoals0,
!:Info = !.Info
),
- AllAtomicGoals0 = [MainGoal0 | OrElseGoals1],
+
+ assoc_list.from_corresponding_lists([MainGoal0 | OrElseGoals1],
+ [Inner | OrElseInners], AtomicGoalsWithInners0),
NonLocalVarSets0 = [],
- implicitly_quantify_disj(AllAtomicGoals0, AllAtomicGoals,
- NonLocalsToRecompute, !Info,
+ implicitly_quantify_atomic_goals(AtomicGoalsWithInners0,
+ AllAtomicGoals, NonLocalsToRecompute, !Info,
NonLocalVarSets0, NonLocalVarSets),
+
(
AllAtomicGoals = [MainGoal | OrElseGoals]
;
@@ -599,9 +604,7 @@ implicitly_quantify_goal_quant_info_2(GoalExpr0, GoalExpr, GoalInfo0,
(
GoalType = unknown_atomic_goal_type,
Outer = atomic_interface_vars(OuterDI, OuterUO),
- Inner = atomic_interface_vars(InnerDI, InnerUO),
- insert_list(NonLocalVars0, [OuterDI, OuterUO], NonLocalVars1),
- delete_list(NonLocalVars1, [InnerDI, InnerUO], NonLocalVars)
+ insert_list(NonLocalVars0, [OuterDI, OuterUO], NonLocalVars)
;
( GoalType = top_level_atomic_goal
; GoalType = nested_atomic_goal
@@ -609,6 +612,7 @@ implicitly_quantify_goal_quant_info_2(GoalExpr0, GoalExpr, GoalInfo0,
NonLocalVars = NonLocalVars0
),
set_nonlocals(NonLocalVars, !Info),
+
ShortHand = atomic_goal(GoalType, Outer, Inner, MaybeOutputVars,
MainGoal, OrElseGoals, OrElseInners),
GoalExpr = shorthand(ShortHand)
@@ -1147,6 +1151,38 @@ implicitly_quantify_disj([Goal0 | Goals0], [Goal | Goals],
implicitly_quantify_disj(Goals0, Goals, NonLocalsToRecompute,
!Info, !NonLocalVarSets).
+:- pred implicitly_quantify_atomic_goals(
+ list(pair(hlds_goal, atomic_interface_vars)), list(hlds_goal),
+ nonlocals_to_recompute, quant_info, quant_info,
+ list(set_of_var), list(set_of_var)).
+:- mode implicitly_quantify_atomic_goals(in, out,
+ in(ordinary_nonlocals_maybe_lambda), in, out, in, out) is det.
+:- mode implicitly_quantify_atomic_goals(in, out,
+ in(ordinary_nonlocals_no_lambda), in, out, in, out) is det.
+:- mode implicitly_quantify_atomic_goals(in, out,
+ in(code_gen_nonlocals_no_lambda), in, out, in, out) is det.
+
+implicitly_quantify_atomic_goals([], [], _, !Info, !NonLocalVarSets).
+implicitly_quantify_atomic_goals([Goal0 - Inner0 | Goals0], [Goal | Goals],
+ NonLocalsToRecompute, !Info, !NonLocalVarSets) :-
+ Goal0 = hlds_goal(_, GoalInfo0),
+ ( goal_info_has_feature(GoalInfo0, feature_contains_stm_inner_outer) ->
+ true
+ ;
+ % The calls to stm_from_outer_to_inner and stm_from_inner_to_outer are
+ % not inserted until the purity checking pass.
+ Inner0 = atomic_interface_vars(InnerDI, InnerUO),
+ get_outside(!.Info, OutsideVars0),
+ insert_list(OutsideVars0, [InnerDI, InnerUO], OutsideVars),
+ set_outside(OutsideVars, !Info)
+ ),
+ implicitly_quantify_goal_quant_info(Goal0, Goal, NonLocalsToRecompute,
+ !Info),
+ get_nonlocals(!.Info, GoalNonLocalVars),
+ !:NonLocalVarSets = [GoalNonLocalVars | !.NonLocalVarSets],
+ implicitly_quantify_atomic_goals(Goals0, Goals, NonLocalsToRecompute,
+ !Info, !NonLocalVarSets).
+
:- pred implicitly_quantify_cases(list(case), list(case),
nonlocals_to_recompute, quant_info, quant_info,
list(set_of_var), list(set_of_var)).
diff --git a/compiler/saved_vars.m b/compiler/saved_vars.m
index 6e0eb7f..04ba0dd 100644
--- a/compiler/saved_vars.m
+++ b/compiler/saved_vars.m
@@ -243,6 +243,7 @@ ok_to_duplicate(feature_contains_trace) = yes.
ok_to_duplicate(feature_pretest_equality) = yes.
ok_to_duplicate(feature_pretest_equality_condition) = yes.
ok_to_duplicate(feature_lambda_undetermined_mode) = yes.
+ok_to_duplicate(feature_contains_stm_inner_outer) = yes.
% Divide a list of goals into an initial subsequence of goals
% that construct constants, and all other goals.
diff --git a/compiler/state_var.m b/compiler/state_var.m
index 0f2302e..d053957 100644
--- a/compiler/state_var.m
+++ b/compiler/state_var.m
@@ -691,12 +691,9 @@ svar_finish_outer_atomic_scope(OuterScopeInfo, !SInfo) :-
before_svar_info :: svar_info
).
-svar_start_inner_atomic_scope(Context, InnerStateVar, InnerScopeInfo,
+svar_start_inner_atomic_scope(_Context, InnerStateVar, InnerScopeInfo,
!VarSet, !SInfo, !Specs) :-
- prepare_for_local_state_vars([InnerStateVar], !VarSet, !SInfo),
- % This mention of !:InnerStateVar is to allow code in the atomic scope
- % to access !.InnerStateVar.
- svar_colon(Context, InnerStateVar, InnerDI, !VarSet, !SInfo, !Specs),
+ new_local_state_var(InnerStateVar, InnerDI, _, !VarSet, !SInfo),
InnerScopeInfo = svar_inner_atomic_scope_info(InnerStateVar, InnerDI,
!.SInfo).
@@ -704,8 +701,7 @@ svar_finish_inner_atomic_scope(Context, InnerScopeInfo, InnerDI, InnerUO,
!VarSet, !SInfo, !Specs) :-
InnerScopeInfo = svar_inner_atomic_scope_info(InnerStateVar, InnerDI,
BeforeSInfo),
- % XXX Should this be svar_dot?
- svar_colon(Context, InnerStateVar, InnerUO, !VarSet, !SInfo, !Specs),
+ svar_dot(Context, InnerStateVar, InnerUO, !VarSet, !SInfo, !Specs),
finish_local_state_vars([InnerStateVar], Vars, BeforeSInfo, !SInfo),
trace [compiletime(flag("atomic_scope_syntax")), io(!IO)] (
( Vars = [Var1, Var2] ->
@@ -714,7 +710,7 @@ svar_finish_inner_atomic_scope(Context, InnerScopeInfo, InnerDI, InnerUO,
io.nl(!IO),
io.write(InnerUO, !IO),
io.nl(!IO),
- io.write_string("finish", !IO),
+ io.write_string("finish:\n", !IO),
io.write(Var1, !IO),
io.nl(!IO),
io.write(Var2, !IO),
diff --git a/compiler/typecheck.m b/compiler/typecheck.m
index a806ff8..ce808d2 100644
--- a/compiler/typecheck.m
+++ b/compiler/typecheck.m
@@ -1329,19 +1329,18 @@ typecheck_goal_2(GoalExpr0, GoalExpr, GoalInfo, !Info) :-
typecheck_goal(MainGoal0, MainGoal, !Info),
typecheck_goal_list(OrElseGoals0, OrElseGoals, !Info),
- InnerVars = atomic_interface_list_to_var_list(
- [Inner | OrElseInners]),
Outer = atomic_interface_vars(OuterDI, OuterUO),
- InterfaceVars = [OuterDI, OuterUO | InnerVars],
- ensure_vars_have_a_type(InterfaceVars, !Info),
+ ensure_vars_have_a_single_type([OuterDI, OuterUO], !Info),
- % The outer variables must either be both I/O states of STM states.
+ % The outer variables must either be both I/O states or STM states.
% Checking that here could double the number of type assign sets.
% We therefore delay the check until after we have typechecked
% the predicate body, in post_typecheck. The code in the
% post_typecheck pass (actually in purity.m) will do this
% if the GoalType is unknown_atomic_goal_type.
- foldl((pred(Var::in, Info0::in, Info::out) is det :-
+ InnerVars = atomic_interface_list_to_var_list(
+ [Inner | OrElseInners]),
+ list.foldl((pred(Var::in, Info0::in, Info::out) is det :-
typecheck_var_has_type(Var, stm_atomic_type, Info0, Info)),
InnerVars, !Info),
expect(unify(GoalType, unknown_atomic_goal_type), this_file,
@@ -1369,6 +1368,7 @@ typecheck_goal_2(GoalExpr0, GoalExpr, GoalInfo, !Info) :-
:- func atomic_interface_list_to_var_list(list(atomic_interface_vars)) =
list(prog_var).
+
atomic_interface_list_to_var_list([]) = [].
atomic_interface_list_to_var_list([atomic_interface_vars(I, O) | Interfaces]) =
[I, O | atomic_interface_list_to_var_list(Interfaces)].
@@ -1407,6 +1407,29 @@ ensure_vars_have_a_type(Vars, !Info) :-
Types, EmptyConstraints, !Info)
).
+ % Ensure that each variable in Vars has been assigned a single type.
+ %
+:- pred ensure_vars_have_a_single_type(list(prog_var)::in,
+ typecheck_info::in, typecheck_info::out) is det.
+
+ensure_vars_have_a_single_type(Vars, !Info) :-
+ (
+ Vars = []
+ ;
+ Vars = [_ | _],
+ % Invent a new type variable to use as the type of these
+ % variables. Since the type is the type of a program variable,
+ % each must have kind `star'.
+ varset.init(TypeVarSet0),
+ varset.new_var(TypeVarSet0, TypeVar, TypeVarSet),
+ Type = type_variable(TypeVar, kind_star),
+ list.length(Vars, NumVars),
+ list.duplicate(NumVars, Type, Types),
+ empty_hlds_constraints(EmptyConstraints),
+ typecheck_var_has_polymorphic_type_list(Vars, TypeVarSet, [],
+ Types, EmptyConstraints, !Info)
+ ).
+
%-----------------------------------------------------------------------------%
:- pred typecheck_higher_order_call(prog_var::in, purity::in,
diff --git a/tests/stm/Mmakefile b/tests/stm/Mmakefile
index 3bcd24d..c0e9781 100644
--- a/tests/stm/Mmakefile
+++ b/tests/stm/Mmakefile
@@ -12,6 +12,8 @@ VALID_PROGS = \
nested \
nested_or_else \
atomic_or_else \
+ atomic_conj \
+ atomic_ite \
#demo \
par-asm_test7 \
par-asm_test8 \
diff --git a/tests/stm/atomic_conj.exp b/tests/stm/atomic_conj.exp
new file mode 100644
index 0000000..1191247
--- /dev/null
+++ b/tests/stm/atomic_conj.exp
@@ -0,0 +1,2 @@
+1
+2
diff --git a/tests/stm/atomic_conj.m b/tests/stm/atomic_conj.m
new file mode 100644
index 0000000..ceffc60
--- /dev/null
+++ b/tests/stm/atomic_conj.m
@@ -0,0 +1,37 @@
+% Two atomic scopes in a conjunction.
+
+:- module atomic_conj.
+:- interface.
+
+:- import_module io.
+
+:- pred main(io::di, io::uo) is cc_multi.
+
+%------------------------------------------------------------------------------%
+%------------------------------------------------------------------------------%
+
+:- implementation.
+
+:- import_module int.
+:- import_module stm_builtin.
+
+%------------------------------------------------------------------------------%
+
+main(IO0, IO) :-
+ new_stm_var(1, Var, IO0, IO1),
+ atomic [outer(IO1, IO2), inner(STM0, STM2)] (
+ read_stm_var(Var, A, STM0, STM1),
+ write_stm_var(Var, A + 1, STM1, STM2)
+ ),
+ atomic [outer(IO2, IO3), inner(STM3, STM)] (
+ read_stm_var(Var, B, STM3, STM)
+ ),
+
+ io.write_int(A, IO3, IO4),
+ io.nl(IO4, IO5),
+ io.write_int(B, IO5, IO6),
+ io.nl(IO6, IO).
+
+%------------------------------------------------------------------------------%
+%------------------------------------------------------------------------------%
+
diff --git a/tests/stm/atomic_ite.exp b/tests/stm/atomic_ite.exp
new file mode 100644
index 0000000..30b148d
--- /dev/null
+++ b/tests/stm/atomic_ite.exp
@@ -0,0 +1,11 @@
+10
+9
+8
+7
+6
+5
+4
+3
+2
+1
+0
diff --git a/tests/stm/atomic_ite.m b/tests/stm/atomic_ite.m
new file mode 100644
index 0000000..832065b
--- /dev/null
+++ b/tests/stm/atomic_ite.m
@@ -0,0 +1,46 @@
+:- module atomic_ite.
+:- interface.
+
+:- import_module io.
+
+:- pred main(io::di, io::uo) is det.
+
+%-----------------------------------------------------------------------------%
+%-----------------------------------------------------------------------------%
+
+:- implementation.
+
+:- import_module int.
+:- import_module stm_builtin.
+
+%-----------------------------------------------------------------------------%
+
+main(!IO) :-
+ new_stm_var(10, Var, !IO),
+ atomic [outer(!IO), inner(!STM)] (
+ countdown(Var, !STM)
+ ).
+
+:- pred countdown(stm_var(int)::in, stm::di, stm::uo) is det.
+
+countdown(Var, !IO) :-
+ atomic [outer(!IO), inner(!STM)] (
+ read_stm_var(Var, X, !STM),
+ ( X < 0 ->
+ retry(!.STM)
+ ;
+ trace [io(!IO)] (
+ io.write_int(X, !IO),
+ io.nl(!IO)
+ ),
+ write_stm_var(Var, X - 1, !STM)
+ )
+ ),
+ ( X = 0 ->
+ true
+ ;
+ countdown(Var, !IO)
+ ).
+
+%-----------------------------------------------------------------------------%
+% vim: ft=mercury ts=8 sts=4 sw=4 et
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------
More information about the reviews
mailing list