support for deterministic tabled calls and answers

This commit is contained in:
Ricardo Rocha 2009-07-03 00:54:39 +01:00
parent cd2902f0d8
commit c666f74532
7 changed files with 266 additions and 90 deletions

10
H/Yap.h
View File

@ -14,6 +14,9 @@
*************************************************************************/
#include "config.h"
#if defined(YAPOR) || defined(TABLING)
#include "opt.config.h"
#endif /* YAPOR || TABLING */
/*
@ -588,13 +591,6 @@ typedef enum
#include "Yapproto.h"
/************************ OPTYap configuration ************************/
/* These must be included before unification handlers */
#if defined(YAPOR) || defined(TABLING)
#include "opt.config.h"
#endif /* YAPOR || TABLING */
/***********************************************************************/
/*

View File

@ -802,8 +802,36 @@ typedef Term *tr_fr_ptr;
Choice Point Structure
6 fixed fields (TR,AP,H,B,ENV,CP) plus arguments
*/
#ifdef DETERMINISTIC_TABLING
struct deterministic_choicept {
yamop *cp_ap;
struct choicept *cp_b;
tr_fr_ptr cp_tr;
#ifdef DEPTH_LIMIT
CELL cp_depth;
#endif /* DEPTH_LIMIT */
#ifdef YAPOR
int cp_lub; /* local untried branches */
struct or_frame *cp_or_fr; /* or-frame pointer */
#endif /* YAPOR */
};
typedef struct choicept {
yamop *cp_ap;
struct choicept *cp_b;
tr_fr_ptr cp_tr;
#ifdef DEPTH_LIMIT
CELL cp_depth;
#endif /* DEPTH_LIMIT */
#ifdef YAPOR
int cp_lub; /* local untried branches */
struct or_frame *cp_or_fr; /* or-frame pointer */
#endif /* YAPOR */
CELL *cp_h;
yamop *cp_cp;
#else
typedef struct choicept {
tr_fr_ptr cp_tr;
CELL *cp_h;
@ -817,6 +845,7 @@ typedef struct choicept {
struct or_frame *cp_or_fr; /* or-frame pointer */
#endif /* YAPOR */
yamop *cp_ap;
#endif /* DETERMINISTIC_TABLING */
#if MIN_ARRAY == 0
CELL *cp_env;
/* GNUCC understands empty arrays */

View File

@ -9,32 +9,29 @@
**********************************************************************/
/* ----------------------------------------------------------------- **
** General Configuration Parameters **
** ----------------------------------------------------------------- */
/* ------------------------------------------ **
** memory alloc scheme (define one) **
** ------------------------------------------ */
#define YAP_MEMORY_ALLOC_SCHEME 1
/* #define SHM_MEMORY_ALLOC_SCHEME 1 */
/* #define MALLOC_MEMORY_ALLOC_SCHEME 1 */
/* ---------------------------------------------------------------- **
** Configuration Parameters **
** TABLING Configuration Parameters **
** ---------------------------------------------------------------- */
/* ----------------------- **
** default sizes **
** ----------------------- */
#define MAX_LENGTH_ANSWER 500
#define MAX_BRANCH_DEPTH 1000
#define MAX_BEST_TIMES 21
#define MAX_TABLE_VARS 100
#define TABLE_LOCK_BUCKETS 512
#define TG_ANSWER_SLOTS 20
/* ----------------------------------------- **
** memory alloc scheme (define one) **
** ----------------------------------------- */
/* #define SHM_MEMORY_ALLOC_SCHEME 1 */
#define YAP_MEMORY_ALLOC_SCHEME 1
/* #define MALLOC_MEMORY_ALLOC_SCHEME 1 */
/* ------------------------------------------- **
** memory mapping scheme (define one) **
** ------------------------------------------- */
#define MMAP_MEMORY_MAPPING_SCHEME 1
/* #define SHM_MEMORY_MAPPING_SCHEME 1 */
#define MAX_TABLE_VARS 100
/* ------------------------------------------ **
** trail freeze scheme (define one) **
@ -42,63 +39,114 @@
#define BFZ_TRAIL_SCHEME 1
/* #define BBREG_TRAIL_SCHEME 1 */
/* ------------------------------------------------------------------ **
** tries locking scheme (define one) **
** ------------------------------------------------------------------ **
** The TABLE_LOCK_AT_ENTRY_LEVEL scheme locks the access to the table **
** space in the entry data structure. It restricts the number of lock **
** operations needed to go through the table data structures. **
** **
** The TABLE_LOCK_AT_NODE_LEVEL scheme locks each data structure **
** before accessing it. It decreases concurrrency for workers **
** accessing commom parts of the table space. **
** **
** The TABLE_LOCK_AT_WRITE_LEVEL scheme is an hibrid scheme, it only **
** locks a table data structure when it is going to update it. You **
** can use ALLOC_BEFORE_CHECK with this scheme to allocate a node **
** before checking if it will be necessary. **
** ------------------------------------------------------------------ */
#define TABLE_LOCK_AT_WRITE_LEVEL 1
/* #define TABLE_LOCK_AT_ENTRY_LEVEL 1 */
/* #define TABLE_LOCK_AT_NODE_LEVEL 1 */
/* #define ALLOC_BEFORE_CHECK 1 */
/* ----------------------------------------------- **
** limit the table space size? (optional) **
** ----------------------------------------------- */
/* ------------------------------------------------ **
** limit the table space size? (optional) **
** ------------------------------------------------ */
/* #define LIMIT_TABLING 1 */
/* ----------------------------------------------- **
** support incomplete tabling? (optional) **
** ----------------------------------------------- */
/* ------------------------------------------------ **
** support incomplete tabling? (optional) **
** ------------------------------------------------ */
/* #define INCOMPLETE_TABLING 1 */
/* ----------------------------------------------- **
** support trie compact lists? (optional) **
** ----------------------------------------------- */
/* ------------------------------------------------ **
** support trie compact lists? (optional) **
** ------------------------------------------------ */
/* #define TRIE_COMPACT_LISTS 1 */
/* --------------------------------------- **
** support inner cuts? (optional) **
** --------------------------------------- */
#define TABLING_INNER_CUTS 1
/* --------------------------------------------------- **
** support deterministic tabling? (optional) **
** --------------------------------------------------- */
/* #define DETERMINISTIC_TABLING 1 */
/* -------------------------------------------------- **
** use timestamps for suspension? (optional) **
** -------------------------------------------------- */
#define TIMESTAMP_CHECK 1
/* ------------------------------------------ **
** enable error checking? (optional) **
** ------------------------------------------ */
/* #define YAPOR_ERRORS 1 */
/* ---------------------------------------- -- **
** enable error checking? (optional) **
** ------------------------------------------- */
/* #define TABLING_ERRORS 1 */
/* -------------------------------------------------------- **
** Parameter Checks **
** -------------------------------------------------------- */
/* ---------------------------------------------------------------- **
** YAPOR Configuration Parameters **
** ---------------------------------------------------------------- */
/* ----------------------- **
** default sizes **
** ----------------------- */
#define MAX_LENGTH_ANSWER 1000
#define MAX_BRANCH_DEPTH 1000
#define MAX_BEST_TIMES 21
/* -------------------------------------------- **
** memory mapping scheme (define one) **
** -------------------------------------------- */
#define MMAP_MEMORY_MAPPING_SCHEME 1
/* #define SHM_MEMORY_MAPPING_SCHEME 1 */
/* ---------------------------------------- -- **
** enable error checking? (optional) **
** ------------------------------------------- */
/* #define YAPOR_ERRORS 1 */
/* ---------------------------------------------------------------- **
** OPTYAP Configuration Parameters **
** ---------------------------------------------------------------- */
/* ----------------------- **
** default sizes **
** ----------------------- */
#define TABLE_LOCK_BUCKETS 512
#define TG_ANSWER_SLOTS 20
/* ------------------------------------------- **
** tries locking scheme (define one) **
** ------------------------------------------- **
** The TABLE_LOCK_AT_ENTRY_LEVEL scheme locks **
** the access to the table space in the entry **
** data structure. It restricts the number of **
** lock operations needed to go through the **
** table data structures. **
** **
** The TABLE_LOCK_AT_NODE_LEVEL scheme locks **
** each data structure before accessing it. It **
** decreases concurrrency for workers **
** accessing commom parts of the table space. **
** **
** The TABLE_LOCK_AT_WRITE_LEVEL scheme is an **
** hibrid scheme, it only locks a table data **
** structure when it is going to update it. **
** You can use ALLOC_BEFORE_CHECK with this **
** scheme to allocate a node before checking **
** if it will be necessary. **
** ------------------------------------------- */
/* #define TABLE_LOCK_AT_ENTRY_LEVEL 1 */
/* #define TABLE_LOCK_AT_NODE_LEVEL 1 */
#define TABLE_LOCK_AT_WRITE_LEVEL 1
/* #define ALLOC_BEFORE_CHECK 1 */
/* ---------------------------------------- **
** support inner cuts? (optional) **
** ---------------------------------------- */
#define TABLING_INNER_CUTS 1
/* --------------------------------------------------- **
** use timestamps for suspension? (optional) **
** --------------------------------------------------- */
#define TIMESTAMP_CHECK 1
/* ---------------------------------------------------------------- **
** Parameter Checks **
** ---------------------------------------------------------------- */
#if !defined(SHM_MEMORY_ALLOC_SCHEME) && !defined(MALLOC_MEMORY_ALLOC_SCHEME) && !defined(YAP_MEMORY_ALLOC_SCHEME)
#error Define a memory alloc scheme
@ -175,6 +223,7 @@
#undef LIMIT_TABLING
#undef INCOMPLETE_TABLING
#undef TRIE_COMPACT_LISTS
#undef DETERMINISTIC_TABLING
#undef TABLING_ERRORS
#endif /* !TABLING */

View File

@ -85,6 +85,30 @@
}
#ifdef DETERMINISTIC_TABLING
#define store_deterministic_generator_node(TAB_ENT, SG_FR) \
{ register choiceptr gcp; \
/* initialize gcp and adjust subgoal frame field */ \
YENV = (CELL *) (DET_GEN_CP(YENV) - 1); \
gcp = NORM_CP(YENV); \
SgFr_gen_cp(SG_FR) = gcp; \
/* store deterministic generator choice point */ \
HBREG = H; \
store_yaam_reg_cpdepth(gcp); \
gcp->cp_tr = TR; \
gcp->cp_ap = COMPLETION; \
gcp->cp_b = B; \
DET_GEN_CP(gcp)->cp_sg_fr = SG_FR; \
store_low_level_trace_info(DET_GEN_CP(gcp), TAB_ENT); \
set_cut((CELL *)gcp, B); \
B = gcp; \
YAPOR_SET_LOAD(B); \
SET_BB(B); \
TABLING_ERRORS_check_stack; \
}
#endif /* DETERMINISTIC_TABLING */
#define restore_generator_node(ARITY, AP) \
{ register CELL *pt_args, *x_args; \
register choiceptr gcp = B; \
@ -372,7 +396,14 @@
/* subgoal new */
init_subgoal_frame(sg_fr);
UNLOCK(SgFr_lock(sg_fr));
store_generator_node(tab_ent, sg_fr, PREG->u.Otapl.s, COMPLETION);
#ifdef DETERMINISTIC_TABLING
if (IsMode_Batched(TabEnt_mode(tab_ent))) {
store_deterministic_generator_node(tab_ent, sg_fr);
} else
#endif /* DETERMINISTIC_TABLING */
{
store_generator_node(tab_ent, sg_fr, PREG->u.Otapl.s, COMPLETION);
}
PREG = PREG->u.Otapl.d; /* should work also with PREG = NEXTOP(PREG,Otapl); */
PREFETCH_OP(PREG);
allocate_environment();
@ -711,6 +742,21 @@
Op(table_trust_me, Otapl)
restore_generator_node(PREG->u.Otapl.s, COMPLETION);
#ifdef DETERMINISTIC_TABLING
if (B_FZ > B && IS_BATCHED_NORM_GEN_CP(B)) {
CELL *subs_ptr = (CELL *)(GEN_CP(B) + 1) + PREG->u.Otapl.s;
choiceptr gcp = NORM_CP(DET_GEN_CP(subs_ptr) - 1);
sg_fr_ptr sg_fr = GEN_CP(B)->cp_sg_fr;
DET_GEN_CP(gcp)->cp_sg_fr = sg_fr;
#ifdef DEPTH_LIMIT
gcp->cp_depth = B->cp_depth;
#endif /* DEPTH_LIMIT */
gcp->cp_tr = B->cp_tr;
gcp->cp_b = B->cp_b;
gcp->cp_ap = B->cp_ap;
SgFr_gen_cp(sg_fr) = B = gcp;
}
#endif /* DETERMINISTIC_TABLING */
YENV = (CELL *) PROTECT_FROZEN_B(B);
set_cut(YENV, B->cp_b);
SET_BB(NORM_CP(YENV));
@ -723,6 +769,21 @@
Op(table_trust, Otapl)
restore_generator_node(PREG->u.Otapl.s, COMPLETION);
#ifdef DETERMINISTIC_TABLING
if (B_FZ > B && IS_BATCHED_NORM_GEN_CP(B)) {
CELL *subs_ptr = (CELL *)(GEN_CP(B) + 1) + PREG->u.Otapl.s;
choiceptr gcp = NORM_CP(DET_GEN_CP(subs_ptr) - 1);
sg_fr_ptr sg_fr = GEN_CP(B)->cp_sg_fr;
DET_GEN_CP(gcp)->cp_sg_fr = sg_fr;
#ifdef DEPTH_LIMIT
gcp->cp_depth = B->cp_depth;
#endif /* DEPTH_LIMIT */
gcp->cp_tr = B->cp_tr;
gcp->cp_b = B->cp_b;
gcp->cp_ap = B->cp_ap;
SgFr_gen_cp(sg_fr) = B = gcp;
}
#endif /* DETERMINISTIC_TABLING */
YENV = (CELL *) PROTECT_FROZEN_B(B);
set_cut(YENV, B->cp_b);
SET_BB(NORM_CP(YENV));
@ -740,8 +801,16 @@
ans_node_ptr ans_node;
gcp = NORM_CP(YENV[E_B]);
sg_fr = GEN_CP(gcp)->cp_sg_fr;
subs_ptr = (CELL *)(GEN_CP(gcp) + 1) + PREG->u.s.s;
#ifdef DETERMINISTIC_TABLING
if (IS_DET_GEN_CP(gcp)){
sg_fr = DET_GEN_CP(gcp)->cp_sg_fr;
subs_ptr = (CELL *)(DET_GEN_CP(gcp) + 1) ;
} else
#endif /* DETERMINISTIC_TABLING */
{
sg_fr = GEN_CP(gcp)->cp_sg_fr;
subs_ptr = (CELL *)(GEN_CP(gcp) + 1) + PREG->u.s.s;
}
#ifdef TABLING_ERRORS
{
sg_fr_ptr aux_sg_fr;
@ -934,6 +1003,13 @@
if (IS_BATCHED_GEN_CP(gcp)) {
/* if the number of substitution variables is zero,
an answer is sufficient to perform an early completion */
#ifdef DETERMINISTIC_TABLING
if (IS_DET_GEN_CP(gcp) && gcp == B) {
private_completion(sg_fr);
B = B->cp_b;
SET_BB(PROTECT_FROZEN_B(B));
} else
#endif /* DETERMINISTIC_TABLING */
if (*subs_ptr == 0 && gcp->cp_ap != NULL) {
gcp->cp_ap = COMPLETION;
mark_as_completed(sg_fr);
@ -1555,7 +1631,12 @@
/* complete all */
sg_fr_ptr sg_fr;
sg_fr = GEN_CP(B)->cp_sg_fr;
#ifdef DETERMINISTIC_TABLING
if (IS_DET_GEN_CP(B))
sg_fr = DET_GEN_CP(B)->cp_sg_fr;
else
#endif /* DETERMINISTIC_TABLING */
sg_fr = GEN_CP(B)->cp_sg_fr;
private_completion(sg_fr);
if (IS_BATCHED_GEN_CP(B)) {
/* backtrack */

View File

@ -61,11 +61,18 @@ STD_PROTO(static inline tg_sol_fr_ptr CUT_prune_tg_solution_frames, (tg_sol_fr_p
** Tabling Macros **
** ----------------------- */
#define NORM_CP(CP) ((choiceptr)(CP))
#define CONS_CP(CP) ((struct consumer_choicept *)(CP))
#define GEN_CP(CP) ((struct generator_choicept *)(CP))
#define LOAD_CP(CP) ((struct loader_choicept *)(CP))
#define IS_BATCHED_GEN_CP(CP) (GEN_CP(CP)->cp_dep_fr == NULL)
#define NORM_CP(CP) ((choiceptr)(CP))
#define GEN_CP(CP) ((struct generator_choicept *)(CP))
#define CONS_CP(CP) ((struct consumer_choicept *)(CP))
#define LOAD_CP(CP) ((struct loader_choicept *)(CP))
#ifdef DETERMINISTIC_TABLING
#define DET_GEN_CP(CP) ((struct deterministic_generator_choicept *)(CP))
#define IS_DET_GEN_CP(CP) (*(CELL*)(DET_GEN_CP(CP) + 1) <= MAX_TABLE_VARS)
#define IS_BATCHED_NORM_GEN_CP(CP) (GEN_CP(CP)->cp_dep_fr == NULL)
#define IS_BATCHED_GEN_CP(CP) (IS_DET_GEN_CP(CP) || IS_BATCHED_NORM_GEN_CP(CP))
#else
#define IS_BATCHED_GEN_CP(CP) (GEN_CP(CP)->cp_dep_fr == NULL)
#endif /* DETERMINISTIC_TABLING */
#define TAG_AS_ANSWER_LEAF_NODE(NODE) TrNode_parent(NODE) = (ans_node_ptr)((unsigned long int)TrNode_parent(NODE) | 0x1)
#define UNTAG_ANSWER_LEAF_NODE(NODE) ((ans_node_ptr)((unsigned long int)NODE & ~(0x1)))
@ -103,7 +110,7 @@ STD_PROTO(static inline tg_sol_fr_ptr CUT_prune_tg_solution_frames, (tg_sol_fr_p
/* LowTagBits is 3 for 32 bit-machines and 7 for 64 bit-machines */
#define NumberOfLowTagBits (LowTagBits == 3 ? 2 : 3)
#define NumberOfLowTagBits (LowTagBits == 3 ? 2 : 3)
#define MakeTableVarTerm(INDEX) (INDEX << NumberOfLowTagBits)
#define VarIndexOfTableTerm(TERM) (TERM >> NumberOfLowTagBits)
#define VarIndexOfTerm(TERM) \

View File

@ -34,14 +34,18 @@
#define SetMode_LoadAnswers(X) (X) |= Mode_LoadAnswers
#define SetMode_ExecAnswers(X) (X) &= ~Mode_LoadAnswers
#define IsMode_Local(X) ((X) & Mode_Local)
#define IsMode_Batched(X) (!IsMode_Local(X))
#define IsMode_LoadAnswers(X) ((X) & Mode_LoadAnswers)
#define IsMode_ExecAnswers(X) (!IsMode_LoadAnswers(X))
#define SetDefaultMode_Local(X) (X) |= DefaultMode_Local
#define SetDefaultMode_Batched(X) (X) &= ~DefaultMode_Local
#define SetDefaultMode_LoadAnswers(X) (X) |= DefaultMode_LoadAnswers
#define SetDefaultMode_ExecAnswers(X) (X) &= ~DefaultMode_LoadAnswers
#define IsDefaultMode_Local(X) ((X) & DefaultMode_Local)
#define IsDefaultMode_Batched(X) (!IsDefaultMode_Local(X))
#define IsDefaultMode_LoadAnswers(X) ((X) & DefaultMode_LoadAnswers)
#define IsDefaultMode_ExecAnswers(X) (!IsDefaultMode_LoadAnswers(X))
@ -307,19 +311,29 @@ typedef struct suspension_frame {
/* --------------------------------------------------------------------------- **
** Structs generator_choicept, consumer_choicept and loader_choicept **
** --------------------------------------------------------------------------- */
/* ------------------------------- **
** Structs choice points **
** ------------------------------- */
struct generator_choicept {
struct choicept cp;
struct dependency_frame *cp_dep_fr; /* NULL if batched scheduling */
struct dependency_frame *cp_dep_fr; /* always NULL if batched scheduling */
struct subgoal_frame *cp_sg_fr;
#ifdef LOW_LEVEL_TRACER
struct pred_entry *cp_pred_entry;
#endif /* LOW_LEVEL_TRACER */
};
#ifdef DETERMINISTIC_TABLING
struct deterministic_generator_choicept {
struct deterministic_choicept cp;
struct subgoal_frame *cp_sg_fr;
#ifdef LOW_LEVEL_TRACER
struct pred_entry *cp_pred_entry;
#endif /* LOW_LEVEL_TRACER */
};
#endif /* DETERMINISTIC_TABLING */
struct consumer_choicept {
struct choicept cp;
struct dependency_frame *cp_dep_fr;

View File

@ -1211,8 +1211,8 @@ static struct trie_statistics{
#define TrStat_ans_max_depth trie_stats.answer_trie_max_depth
#define TrStat_ans_min_depth trie_stats.answer_trie_min_depth
#define STR_ARRAY_SIZE 10000
#define ARITY_ARRAY_SIZE 1000
#define STR_ARRAY_SIZE 100000
#define ARITY_ARRAY_SIZE 10000
#define SHOW_TABLE(MESG, ARGS...) if (TrStat_show) fprintf(Yap_stdout, MESG, ##ARGS)