mercurylang/mercury
1
0
Fork 0
mirror of https://github.com/Mercury-Language/mercury.git synced 2025-12-13 04:44:39 +00:00
Code Issues Projects Releases Wiki Activity

Add support for thread-local backjumping in grades that support concurrency.

Browse Source 
Estimated hours taken: 7
Branches: main

Add support for thread-local backjumping in grades that support concurrency.

library/backjump.m:
	Shift the C definition of backjump handlers and choice ids into the
	runtime.  This is needed because MR_Context now refers to them and
	the runtime should not depend on the library.

	Delete the XXX comment regarding pred_is_external/3.  (This has been
	fixed below.)

runtime/mercury_backjump.h:
runtime/mercury_backjump.c:
	New module that defines those parts of the backjumping support that
	the runtime requires access to.

	In high-level C .par grades make the global state required by
	backjumping thread-specific.

	Conform to the usual coding conventions in the runtime in the new
	versions of the data structures that were originally in backjump.m.

	Rename ML_Choice_Id to MR_BackJumpChoiceId, the latter is less
	ambiguous.

runtime/mercury_context.h:
runtime/mercury_context.c:
	In low-level C grades add two extra fields to the MR_Context structure
	to hold the global state required by backjumping.

	In high-level C .par grades initialise the the thread-specific data that
	is used to store the backjump global state at program startup.

	Reformat a function prototype.

runtime/mercury_thread.h:
	Reformat a function prototype.

runtime/Mmakefile:
	Include the new files.

mdbcomp/program_representation.m:
	Update pred_is_external/3 to include backjump.builtin_choice_id/1
	and backjump.builtin_backjump/1.

tests/hard_coded/Mmakefile:
tests/hard_coded/tl_backjump_test.m:
tests/hard_coded/tl_backjump_test.exp:
	Test thread-local backjumping.

tests/hard_coded/tl_backjump_test.exp2:
	Expected output for the above test case for grades in which spawn/3
	does not work.
This commit is contained in:
Julien Fischer
2008-03-19 05:30:01 +00:00
parent 6cbafb4e96
commit 5c49b5dac9
12 changed files with 408 additions and 77 deletions
Download Patch File Download Diff File Expand all files Collapse all files

112
library/backjump.m
View File

@@ -112,53 +112,13 @@ backjump(Id) :-
% mdbcomp/program_representation.m. The debugger needs to know what predicates
% are defined externally, so that it knows not to expect events for those
% predicates.
%
% XXX we haven't done this yet.
%
:- external(builtin_choice_id/1).
:- external(builtin_backjump/1).
%-----------------------------------------------------------------------------%
:- pragma foreign_decl("C", "
typedef MR_Integer ML_Choice_Id;
typedef struct ML_BackJumpHandler_struct {
struct ML_BackJumpHandler_struct *prev;
ML_Choice_Id id;
#ifdef MR_HIGHLEVEL_CODE
jmp_buf handler;
#else /* !MR_HIGHLEVEL_CODE */
MR_Word *saved_sp;
MR_Word *saved_fr;
#endif /* !MR_HIGHLEVEL_CODE */
} ML_BackJumpHandler;
/*
** XXX Does not work properly in grades that support multiple threads.
*/
#define ML_GET_BACKJUMP_HANDLER() ML_backjump_handler
#define ML_SET_BACKJUMP_HANDLER(val) ML_backjump_handler = (val)
#define ML_GET_NEXT_CHOICE_ID() (ML_next_choice_id++)
extern ML_BackJumpHandler *ML_backjump_handler;
extern ML_Choice_Id ML_next_choice_id;
").
:- pragma foreign_code("C", "
ML_BackJumpHandler *ML_backjump_handler;
ML_Choice_Id ML_next_choice_id = 0;
").
:- pragma foreign_decl("C", "#include \"mercury_backjump.h\"").
%-----------------------------------------------------------------------------%
%
@@ -188,10 +148,10 @@ extern ML_Choice_Id ML_next_choice_id;
#endif
void MR_CALL
mercury__backjump__builtin_choice_id_1_p_0(ML_Choice_Id *id, MR_CONT_PARAMS);
mercury__backjump__builtin_choice_id_1_p_0(MR_BackJumpChoiceId *id, MR_CONT_PARAMS);
void MR_CALL
mercury__backjump__builtin_backjump_1_p_0(ML_Choice_Id id);
mercury__backjump__builtin_backjump_1_p_0(MR_BackJumpChoiceId id);
#endif /* MR_HIGHLEVEL_CODE */
#endif /* ML_BACKJUMP_GUARD */
@@ -213,18 +173,18 @@ mercury__backjump__builtin_backjump_1_p_0(ML_Choice_Id id);
void MR_CALL
mercury__backjump__builtin_choice_id_1_p_0(MR_Integer *id, MR_CONT_PARAMS)
{
ML_BackJumpHandler this_handler;
MR_BackJumpHandler this_handler;
this_handler.prev = ML_GET_BACKJUMP_HANDLER();
this_handler.id = ML_GET_NEXT_CHOICE_ID();
ML_SET_BACKJUMP_HANDLER(&this_handler);
this_handler.MR_bjh_prev = MR_GET_BACKJUMP_HANDLER();
this_handler.MR_bjh_id = MR_GET_NEXT_CHOICE_ID();
MR_SET_BACKJUMP_HANDLER(&this_handler);
if (setjmp(this_handler.handler) == 0) {
if (setjmp(this_handler.MR_bjh_handler) == 0) {
#ifdef MR_DEBUG_JMPBUFS
fprintf(stderr, ""choice setjmp %p\\n"", this_handler.handler);
#endif
*id = this_handler.id;
*id = this_handler.MR_bjh_id;
MR_CONT_CALL();
} else {
#ifdef MR_DEBUG_JMPBUFS
@@ -232,13 +192,15 @@ mercury__backjump__builtin_choice_id_1_p_0(MR_Integer *id, MR_CONT_PARAMS)
#endif
}
ML_SET_BACKJUMP_HANDLER(this_handler.prev);
MR_SET_BACKJUMP_HANDLER(this_handler.MR_bjh_prev);
}
void MR_CALL
mercury__backjump__builtin_backjump_1_p_0(ML_Choice_Id id)
mercury__backjump__builtin_backjump_1_p_0(MR_BackJumpChoiceId id)
{
ML_BackJumpHandler *backjump_handler = ML_GET_BACKJUMP_HANDLER();
MR_BackJumpHandler *backjump_handler;
backjump_handler = MR_GET_BACKJUMP_HANDLER();
/*
** XXX when we commit and prune away nondet stack frames, we leave the
@@ -260,10 +222,10 @@ mercury__backjump__builtin_backjump_1_p_0(ML_Choice_Id id)
** commits.)
*/
while (backjump_handler != NULL) {
if (backjump_handler->id == id) {
if (backjump_handler->MR_bjh_id == id) {
break;
}
backjump_handler = backjump_handler->prev;
backjump_handler = backjump_handler->MR_bjh_prev;
}
if (backjump_handler == NULL) {
@@ -272,9 +234,10 @@ mercury__backjump__builtin_backjump_1_p_0(ML_Choice_Id id)
} else {
#ifdef MR_DEBUG_JMPBUFS
fprintf(stderr, ""backjump longjmp %p\\n"", backjump_handler->handler);
fprintf(stderr, ""backjump longjmp %p\\n"",
backjump_handler->MR_bjh_handler);
#endif
longjmp(backjump_handler->handler, 1);
longjmp(backjump_handler->MR_bjh_handler, 1);
}
}
@@ -313,7 +276,7 @@ void mercury_sys_init_backjumps_write_out_proc_statics(FILE *deep_fp,
#define ML_DUMMY_LINE 0
#define ML_BACKJUMP_STRUCT \
(((ML_BackJumpHandler *) (MR_curfr + 1 - MR_NONDET_FIXED_SIZE)) - 1)
(((MR_BackJumpHandler *) (MR_curfr + 1 - MR_NONDET_FIXED_SIZE)) - 1)
#ifdef ML_DEBUG_BACKJUMPS
#define ML_BACKJUMP_CHECKPOINT(s, p) \
@@ -321,7 +284,8 @@ void mercury_sys_init_backjumps_write_out_proc_statics(FILE *deep_fp,
fflush(stdout); \
fprintf(stderr, ""backjumps (%s): "" \
""loc %p, prev %p, id %d, sp %p, fr %p\\n"", \
s, p, p->prev, p->id, p->saved_sp, p->saved_fr); \
s, p, p->MR_bjh_prev, p->MR_bjh_id, p->MR_bjh_saved_sp, \
p->MR_bjh_saved_fr); \
} while (0)
#else
#define ML_BACKJUMP_CHECKPOINT(s, p)
@@ -355,43 +319,45 @@ MR_BEGIN_CODE
MR_define_entry(mercury__backjump__builtin_choice_id_1_0);
{
MR_mkpragmaframe(""builtin_choice_id/1"", 0, ML_BackJumpHandler_struct,
MR_mkpragmaframe(""builtin_choice_id/1"", 0, MR_BackJumpHandler_Struct,
MR_LABEL(mercury__backjump__builtin_choice_id_1_0_i1));
ML_BACKJUMP_STRUCT->prev = ML_GET_BACKJUMP_HANDLER();
ML_BACKJUMP_STRUCT->id = ML_GET_NEXT_CHOICE_ID();
ML_BACKJUMP_STRUCT->saved_sp = MR_sp;
ML_BACKJUMP_STRUCT->saved_fr = MR_curfr;
ML_SET_BACKJUMP_HANDLER(ML_BACKJUMP_STRUCT);
ML_BACKJUMP_STRUCT->MR_bjh_prev = MR_GET_BACKJUMP_HANDLER();
ML_BACKJUMP_STRUCT->MR_bjh_id = MR_GET_NEXT_CHOICE_ID();
ML_BACKJUMP_STRUCT->MR_bjh_saved_sp = MR_sp;
ML_BACKJUMP_STRUCT->MR_bjh_saved_fr = MR_curfr;
MR_SET_BACKJUMP_HANDLER(ML_BACKJUMP_STRUCT);
ML_BACKJUMP_CHECKPOINT(""create"", ML_BACKJUMP_STRUCT);
MR_r1 = (MR_Word) ML_BACKJUMP_STRUCT->id;
MR_r1 = (MR_Word) ML_BACKJUMP_STRUCT->MR_bjh_id;
MR_succeed();
}
MR_define_label(mercury__backjump__builtin_choice_id_1_0_i1);
{
/* Restore the previous handler. */
ML_SET_BACKJUMP_HANDLER(ML_BACKJUMP_STRUCT->prev);
MR_SET_BACKJUMP_HANDLER(ML_BACKJUMP_STRUCT->MR_bjh_prev);
MR_fail();
}
MR_define_entry(mercury__backjump__builtin_backjump_1_0);
{
ML_Choice_Id id = MR_r1;
ML_BackJumpHandler *backjump_handler = ML_GET_BACKJUMP_HANDLER();
MR_BackJumpChoiceId id = MR_r1;
MR_BackJumpHandler *backjump_handler;
backjump_handler = MR_GET_BACKJUMP_HANDLER();
/*
** XXX see comments in the high-level implementation.
*/
while (backjump_handler != NULL) {
if (backjump_handler->id == id) {
if (backjump_handler->MR_bjh_id == id) {
break;
}
ML_BACKJUMP_CHECKPOINT(""scan"", backjump_handler);
backjump_handler = backjump_handler->prev;
backjump_handler = backjump_handler->MR_bjh_prev;
}
if (backjump_handler == NULL) {
@@ -406,9 +372,9 @@ MR_define_entry(mercury__backjump__builtin_backjump_1_0);
** (possibly incorrect) backjump.
*/
ML_SET_BACKJUMP_HANDLER(backjump_handler->prev);
MR_sp_word = (MR_Word) backjump_handler->saved_sp;
MR_maxfr_word = (MR_Word) backjump_handler->saved_fr;
MR_SET_BACKJUMP_HANDLER(backjump_handler->MR_bjh_prev);
MR_sp_word = (MR_Word) backjump_handler->MR_bjh_saved_sp;
MR_maxfr_word = (MR_Word) backjump_handler->MR_bjh_saved_fr;
MR_fail();
}
}

2
mdbcomp/program_representation.m
View File

@@ -1319,6 +1319,8 @@ pred_is_external("exception", "builtin_throw", 1).
pred_is_external("builtin", "unify", 3).
pred_is_external("builtin", "compare", 4).
pred_is_external("builtin", "compare_representation", 4).
pred_is_external("backjump", "builtin_choice_id", 1).
pred_is_external("backjump", "builtin_backjump", 1).
%-----------------------------------------------------------------------------%

2
runtime/Mmakefile
View File

@@ -26,6 +26,7 @@ HDRS = \
mercury_agc_debug.h \
mercury_array_macros.h \
mercury_atomic_ops.h \
mercury_backjump.h \
mercury_bootstrap.h \
mercury_builtin_types.h \
mercury_builtin_types_proc_layouts.h \
@@ -150,6 +151,7 @@ CFILES = \
mercury_accurate_gc.c \
mercury_agc_debug.c \
mercury_atomic_ops.c \
mercury_backjump.c \
mercury_bootstrap.c \
mercury_builtin_types.c \
mercury_bitmap.c \

53
runtime/mercury_backjump.c Normal file
View File

@@ -0,0 +1,53 @@
/*
** vim: ts=4 sw=4 expandtab
*/
/*
** Copyright (C) 2008 The University of Melbourne.
** This file may only be copied under the terms of the GNU Library General
** Public License - see the file COPYING.LIB in the Mercury distribution.
*/
#include "mercury_backjump.h"
#include "mercury_thread.h"
#if defined(MR_THREAD_SAFE)
#include <pthread.h>
#endif
/*
** The low-level C counterparts to these globals are the `backjump_handler'
** and `backjump_next_choice_id' fields of the MR_Context structure.
** (See mercury_context.h for details.)
*/
#if defined(MR_HIGHLEVEL_CODE)
#if defined(MR_THREAD_SAFE)
MercuryThreadKey MR_backjump_handler_key;
MercuryThreadKey MR_backjump_next_choice_id_key;
#else /* not MR_THREAD_SAFE */
MR_BackJumpHandler *MR_backjump_handler;
MR_BackJumpChoiceId MR_backjump_next_choice_id = 0;
#endif /* not MR_THREAD_SAFE */
#endif /* not MR_HIGHLEVEL_CODE */
#if defined(MR_HIGHLEVEL_CODE) && defined(MR_THREAD_SAFE)
MR_BackJumpChoiceId
MR_get_tl_backjump_next_choice_id(void)
{
MR_BackJumpChoiceId new_choice_id;
/* NOTE: this only works because sizeof(MR_Integer) == sizeof(void *). */
new_choice_id = (MR_Integer) MR_GETSPECIFIC(MR_backjump_next_choice_id_key);
pthread_setspecific(MR_backjump_next_choice_id_key,
(void *)(new_choice_id + 1));
return new_choice_id;
}
#endif /* MR_HIGLEVEL_CODE && MR_THREAD_SAFE */
/*---------------------------------------------------------------------------*/

109
runtime/mercury_backjump.h Normal file
View File

@@ -0,0 +1,109 @@
/*
** vim:ts=4 sw=4 expandtab
*/
/*
** Copyright (C) 2008 The University of Melbourne.
** This file may only be copied under the terms of the GNU Library General
** Public License - see the file COPYING.LIB in the Mercury distribution.
*/
/*
** mercury_backjump.h - code for handling backjumping.
*/
#ifndef MERCURY_BACKJUMP_H
#define MERCURY_BACKJUMP_H
#include "mercury_conf.h"
#include "mercury_thread.h"
#include <setjmp.h>
typedef MR_Integer MR_BackJumpChoiceId;
typedef struct MR_BackJumpHandler_Struct {
struct MR_BackJumpHandler_Struct *MR_bjh_prev;
MR_BackJumpChoiceId MR_bjh_id;
#ifdef MR_HIGHLEVEL_CODE
jmp_buf MR_bjh_handler;
#else /* !MR_HIGHLEVEL_CODE */
MR_Word *MR_bjh_saved_sp;
MR_Word *MR_bjh_saved_fr;
#endif /* !MR_HIGHLEVEL_CODE */
} MR_BackJumpHandler;
/*---------------------------------------------------------------------------*/
/*
** This section defines the global state required to support backjumping.
** In low-level C grades this state is part of the MR_Context structure
** (see mercury_context.h). In non .par high-level C grades we store the
** state in global variables and in .par high-level C grades we need to use
** thread-local data.
*/
#if defined(MR_HIGHLEVEL_CODE)
#if defined(MR_THREAD_SAFE)
extern MR_BackJumpChoiceId
MR_get_tl_backjump_next_choice_id(void);
/*
** MR_backjump_handler_key stores a key that can be used to get
** the current backjump handler for the current thread.
** MR_backjump_next_choice_id_key stores a key that can be used
** to get the next available backjump choice id for the current thread.
** NOTE: changes here may need to be reflected in the function
** MR_init_thread_stuff() in mercury_context.c.
*/
extern MercuryThreadKey MR_backjump_handler_key;
extern MercuryThreadKey MR_backjump_next_choice_id_key;
#define MR_GET_BACKJUMP_HANDLER() \
MR_GETSPECIFIC(MR_backjump_handler_key)
#define MR_SET_BACKJUMP_HANDLER(val) \
pthread_setspecific(MR_backjump_handler_key, (val))
#define MR_GET_NEXT_CHOICE_ID() \
MR_get_tl_backjump_next_choice_id()
#else /* not MR_THREAD_SAFE */
/*
** MR_backjump_handler points to the current backjump handler.
*/
extern MR_BackJumpHandler *MR_backjump_handler;
/*
** The value MR_backjump_next_choice_id is the next available
** backjump choice id.
*/
extern MR_BackJumpChoiceId MR_backjump_next_choice_id;
#define MR_GET_BACKJUMP_HANDLER() MR_backjump_handler
#define MR_SET_BACKJUMP_HANDLER(val) MR_backjump_handler = (val)
#define MR_GET_NEXT_CHOICE_ID() (MR_backjump_next_choice_id++)
#endif /* not MR_THREAD_SAFE */
#else /* not MR_HIGHLEVEL_CODE */
#define MR_GET_BACKJUMP_HANDLER() \
MR_ENGINE(MR_eng_this_context)->MR_ctxt_backjump_handler
#define MR_SET_BACKJUMP_HANDLER(val) \
MR_ENGINE(MR_eng_this_context)->MR_ctxt_backjump_handler = (val)
#define MR_GET_NEXT_CHOICE_ID() \
(MR_ENGINE(MR_eng_this_context)->MR_ctxt_backjump_next_choice_id++)
#endif /* not MR_HIGHLEVEL_CODE */
#endif /* not MERCURY_BACKJUMP_H */

15
runtime/mercury_context.c
View File

@@ -33,8 +33,9 @@ ENDINIT
#include "mercury_engine.h" /* for `MR_memdebug' */
#include "mercury_reg_workarounds.h" /* for `MR_fd*' stuff */
static void MR_init_context_maybe_generator(MR_Context *c,
const char *id, MR_GeneratorPtr gen);
static void
MR_init_context_maybe_generator(MR_Context *c, const char *id,
MR_GeneratorPtr gen);
/*---------------------------------------------------------------------------*/
@@ -104,6 +105,11 @@ MR_init_thread_stuff(void)
#endif
MR_KEY_CREATE(&MR_exception_handler_key, NULL);
#ifdef MR_HIGHLEVEL_CODE
MR_KEY_CREATE(&MR_backjump_handler_key, NULL);
MR_KEY_CREATE(&MR_backjump_next_choice_id_key, (void *)0);
#endif
/* These are actually in mercury_thread.c. */
pthread_mutex_init(&MR_thread_barrier_lock, MR_MUTEX_ATTR);
#ifdef MR_HIGHLEVEL_CODE
@@ -278,6 +284,11 @@ MR_init_context_maybe_generator(MR_Context *c, const char *id,
c->MR_ctxt_ticket_high_water = 1;
#endif
#ifndef MR_HIGHLEVEL_CODE
c->MR_ctxt_backjump_handler = NULL;
c->MR_ctxt_backjump_next_choice_id = 0;
#endif
#ifndef MR_CONSERVATIVE_GC
if (gen != NULL) {
MR_fatal_error("MR_init_context: generator and no conservative gc");

11
runtime/mercury_context.h
View File

@@ -58,6 +58,7 @@
#include "mercury_thread.h" /* for MercuryLock */
#include "mercury_goto.h" /* for MR_GOTO() */
#include "mercury_conf.h" /* for MR_CONSERVATIVE_GC */
#include "mercury_backjump.h" /* for MR_BackJumpHandler, etc */
#ifdef MR_THREAD_SAFE
#define MR_IF_THREAD_SAFE(x) x
@@ -181,6 +182,11 @@
** ticket_highwater The saved MR_ticket_high_water for this context.
** (All accessed via abstract machine register.)
**
** backjump_handler The backjump handler for this context.
** backjump_next_choice_id The next available backjump choice id counter
** for this context.
** (All accessed via MR_eng_context.)
**
** hp The saved hp for this context.
** (Accessed via abstract machine register.)
**
@@ -303,6 +309,11 @@ struct MR_Context_Struct {
MR_ChoicepointId MR_ctxt_ticket_high_water;
#endif
#ifndef MR_HIGHLEVEL_CODE
MR_BackJumpHandler *MR_ctxt_backjump_handler;
MR_BackJumpChoiceId MR_ctxt_backjump_next_choice_id;
#endif
#ifndef MR_CONSERVATIVE_GC
MR_Word *MR_ctxt_hp;
MR_Word *MR_ctxt_min_hp_rec;

3
runtime/mercury_thread.h
View File

@@ -244,7 +244,8 @@ extern MR_Unsigned MR_num_thread_local_mutables;
/*
** Allocate an index into the thread-local mutable array for a mutable.
*/
extern MR_Unsigned MR_new_thread_local_mutable_index(void);
extern MR_Unsigned
MR_new_thread_local_mutable_index(void);
/*
** Allocate a thread-local mutable array.

19
tests/hard_coded/Mmakefile
View File

@@ -473,6 +473,8 @@ endif
# defined.
#
# backjump_test fails because deep profiler cannot yet handle backjumps.
# tl_backjump_test fails because the deep profiler cannot yet handle
# backjumps and threads.
ifeq "$(findstring profdeep,$(GRADE))" ""
NON_PROFDEEP_PROGS = \
@@ -491,6 +493,7 @@ ifeq "$(findstring profdeep,$(GRADE))" ""
solver_default_eq_cmp \
test_array2d \
test_injection \
tl_backjump_test \
user_defined_equality \
version_array_test \
write_binary
@@ -670,7 +673,7 @@ no_fully_strict.out: no_fully_strict
< $@.tmp > $@; \
rm -f $@.tmp; \
fi
# final_excp.out is expected to fail (it calls throw/1).
#
final_excp.out: final_excp
@@ -743,6 +746,20 @@ runtime_opt.out: runtime_opt runtime_opt.inp
done \
) > runtime_opt.out 2>&1
# The test checks the output from multiple threads and since that output
# may be interleaved arbitrarily we need to filter it so that all the output
# from each thread appears sequentially in a block.
tl_backjump_test.out: tl_backjump_test
if ./tl_backjump_test > $@.tmp 2>&1; then \
grep "^(TID: #2" $@.tmp > $@; \
grep "^(TID: #3" $@.tmp >> $@; \
grep "^spawn" $@.tmp >> $@; \
rm -f $@.tmp; \
else \
grep . $@.tmp; \
exit 1; \
fi
#-----------------------------------------------------------------------------#
dir_test.out: prepare_for_dir_test

50
tests/hard_coded/tl_backjump_test.exp Normal file
View File

@@ -0,0 +1,50 @@
(TID: #2) label A = 1, (0)
(TID: #2) label B = 1, (1)
(TID: #2) label C = 1, (2)
(TID: #2) label C = 2, (3)
(TID: #2) backjump (3)
(TID: #2) label C = 3, (4)
(TID: #2) solution 1, 1, 3
(TID: #2) label B = 2, (5)
(TID: #2) label C = 1, (6)
(TID: #2) backjump (0)
(TID: #2) label A = 2, (7)
(TID: #2) label B = 1, (8)
(TID: #2) label C = 1, (9)
(TID: #2) solution 2, 1, 1
(TID: #2) label C = 2, (10)
(TID: #2) backjump (8)
(TID: #2) label B = 2, (11)
(TID: #2) label C = 1, (12)
(TID: #2) label C = 2, (13)
(TID: #2) solution 2, 2, 2
(TID: #2) label C = 3, (14)
(TID: #2) Solutions:
(TID: #2) {1, 1, 3},
(TID: #2) {2, 1, 1},
(TID: #2) {2, 2, 2}
(TID: #3) label A = 1, (0)
(TID: #3) label B = 1, (1)
(TID: #3) label C = 1, (2)
(TID: #3) label C = 2, (3)
(TID: #3) backjump (3)
(TID: #3) label C = 3, (4)
(TID: #3) solution 1, 1, 3
(TID: #3) label B = 2, (5)
(TID: #3) label C = 1, (6)
(TID: #3) backjump (0)
(TID: #3) label A = 2, (7)
(TID: #3) label B = 1, (8)
(TID: #3) label C = 1, (9)
(TID: #3) solution 2, 1, 1
(TID: #3) label C = 2, (10)
(TID: #3) backjump (8)
(TID: #3) label B = 2, (11)
(TID: #3) label C = 1, (12)
(TID: #3) label C = 2, (13)
(TID: #3) solution 2, 2, 2
(TID: #3) label C = 3, (14)
(TID: #3) Solutions:
(TID: #3) {1, 1, 3},
(TID: #3) {2, 1, 1},
(TID: #3) {2, 2, 2}

1
tests/hard_coded/tl_backjump_test.exp2 Normal file
View File

@@ -0,0 +1 @@
spawn/3 not supported in this grade

108
tests/hard_coded/tl_backjump_test.m Normal file
View File

@@ -0,0 +1,108 @@
%---------------------------------------------------------------------------%
% vim: ft=mercury ts=4 sw=4 et
%---------------------------------------------------------------------------%
%
% Test for thread-local backjumping.
%
%---------------------------------------------------------------------------%
%---------------------------------------------------------------------------%
:- module tl_backjump_test.
:- interface.
:- import_module io.
:- pred main(io::di, io::uo) is cc_multi.
:- implementation.
:- import_module backjump.
:- import_module list.
:- import_module solutions.
:- import_module string.
:- import_module thread.
main(!IO) :-
( can_spawn ->
thread.spawn(run_problem(2), !IO),
thread.spawn(run_problem(3), !IO)
;
io.write_string("spawn/3 not supported in this grade", !IO)
).
:- type thread_id == int.
:- pred run_problem(thread_id::in, io::di, io::uo) is cc_multi.
run_problem(TId0, !IO) :-
cc_multi_equal(TId0, TId), % Make sure we are cc_multi.
solutions(problem(TId), Sols),
(
Sols = [],
io.format("(TID: #%d) No solutions!\n",
[i(TId)], !IO)
;
Sols = [_ | _],
io.format("(TID: #%d) Solutions:\n", [i(TId)], !IO),
WriteSoln = (pred(Sol::in, !.IO::di, !:IO::uo) is det :-
io.format("(TID: #%d) ", [i(TId)], !IO),
io.write(Sol, !IO)
),
io.write_list(Sols, ",\n", WriteSoln, !IO),
io.nl(!IO)
).
:- pred problem(thread_id::in, {int, int, int}::out) is nondet.
problem(TId, {A, B, C}) :-
promise_pure (
impure label(TId, "A", [1, 2], A, PA),
impure label(TId, "B", [1, 2], B, PB),
impure label(TId, "C", [1, 2, 3], C, PC),
impure check(TId, A, B, C, PA, PB, PC)
).
:- impure pred label(thread_id::in, string::in, list(int)::in, int::out,
choice_id::out) is nondet.
label(TId, Name, [N | _], N, P) :-
impure get_choice_id(P),
trace [io(!IO)] (
io.format("(TID: #%d) label %s = %d, (%d)\n",
[i(TId), s(Name), i(N), i(to_int(P))], !IO),
true
).
label(TId, Name, [_ | Ns], N, P) :-
impure label(TId, Name, Ns, N, P).
:- impure pred check(thread_id::in, int::in, int::in, int::in, choice_id::in,
choice_id::in, choice_id::in) is semidet.
check(TId, A, B, C, PA, PB, PC) :-
( is_nogood(A, B, C, PA, PB, PC, P) ->
trace [io(!IO)] (
io.format("(TID: #%d) backjump (%d)\n", [i(TId), i(to_int(P))],
!IO)
),
impure backjump(P)
;
is_solution(A, B, C),
trace [io(!IO)] (
io.format("(TID: #%d) solution %d, %d, %d\n",
[i(TId), i(A), i(B), i(C)], !IO)
)
).
:- pred is_nogood(int::in, int::in, int::in, choice_id::in, choice_id::in,
choice_id::in, choice_id::out) is semidet.
is_nogood(1, 1, 2, _, _, P, P).
is_nogood(1, 2, 1, P, _, _, P).
is_nogood(2, 1, 2, _, P, _, P).
:- pred is_solution(int::in, int::in, int::in) is semidet.
is_solution(1, 1, 3).
is_solution(2, 1, 1).
is_solution(2, 2, 2).