From 60b17358a69bb6b9e905f720673519390f7c106d Mon Sep 17 00:00:00 2001 From: bjs Date: Thu, 7 Mar 2024 17:14:53 +0000 Subject: [PATCH] (concretization/random) fix: understand owned vs pinned variables properly --- .../litmus_test_random_concretization.c | 64 +++++++++++-------- lib/litmus_test/litmus_test_var_info.c | 12 ++-- 2 files changed, 44 insertions(+), 32 deletions(-) diff --git a/lib/litmus_test/concretization/litmus_test_random_concretization.c b/lib/litmus_test/concretization/litmus_test_random_concretization.c index bfc93da4..6d921dc7 100644 --- a/lib/litmus_test/concretization/litmus_test_random_concretization.c +++ b/lib/litmus_test/concretization/litmus_test_random_concretization.c @@ -21,26 +21,17 @@ typedef struct { var_st_t var_sts[]; } concretization_st_t; -u8 overlaps_owned_region(concretization_st_t* st, var_info_t* var, var_info_t* with) { - if (with->ty != VAR_HEAP) { +u8 overlaps_owned_regions(concretization_st_t* st, var_info_t* var, var_info_t* with) { + if (!var_owns_region(var) || !var_owns_region(with)) return 0; - } - /* if var overlaps, but is pinned to with - * then it doesn't count as overlapping - */ - if (var->ty == VAR_PINNED && var->pin.pin_region_var == with->varidx) { - if ((int)var->pin.pin_region_level <= (int)with->heap.owned_region_size) { - return 0; - } - } + own_level_t with_region = var_owned_region_size(with); u64 va = st->var_sts[var->varidx].va; u64 otherva = st->var_sts[with->varidx].va; - u64 level = with->heap.owned_region_size; - u64 lo = otherva & ~BITMASK(LEVEL_SHIFTS[level]); - u64 hi = lo + LEVEL_SIZES[level]; + u64 lo = otherva & ~BITMASK(LEVEL_SHIFTS[with_region]); + u64 hi = lo + LEVEL_SIZES[with_region]; if (lo <= va && va < hi) { return 1; @@ -56,14 +47,26 @@ u8 has_same_va(concretization_st_t* st, var_info_t* var, var_info_t* with) { return (va == otherva); } +u8 __can_virtually_alias_with(concretization_st_t* st, var_info_t* var, var_info_t* with) { + return ( + (var->ty == VAR_PINNED) + && (var->pin.pin_region_var == with->varidx) + && (var->pin.pin_region_level == REGION_SAME_VAR) + ); +} + +u8 can_virtually_alias(concretization_st_t* st, var_info_t* var, var_info_t* with) { + return __can_virtually_alias_with(st, var, with) || __can_virtually_alias_with(st, with, var); +} + u8 validate_selection(test_ctx_t* ctx, concretization_st_t* st, var_info_t* thisvar) { var_info_t* var; FOREACH_HEAP_VAR(ctx, var) { if (var->varidx == thisvar->varidx) continue; - if ( has_same_va(st, thisvar, var) - || overlaps_owned_region(st, thisvar, var) + if ( (has_same_va(st, thisvar, var) && !can_virtually_alias(st, thisvar, var)) + || overlaps_owned_regions(st, thisvar, var) ) { debug("OVERLAPS between %s and %s\n", thisvar->name, var->name); return 0; @@ -102,7 +105,7 @@ void pick_pin(test_ctx_t* ctx, concretization_st_t* st, var_info_t* rootvar, reg st->var_sts[pinnedvar->varidx].picked = 1; - DEBUG(DEBUG_CONCRETIZATION, "picked! %s => %p\n", pinnedvar->name, st->var_sts[pinnedvar->varidx].va); + DEBUG(DEBUG_CONCRETIZATION, "picked pin! %s => %p\n", pinnedvar->name, st->var_sts[pinnedvar->varidx].va); } /** select the VA for a var that OWNs a region @@ -193,29 +196,34 @@ void concretize_random_one(test_ctx_t* ctx, const litmus_test_t* cfg, concretiza } } - /* pick the heap vars that are constrained */ + /* pick the heap vars that are constrained + * and any that are pinned to those + * this should pick any HEAP,UNMAPPED or FIXED regions + * and any PINNED vars within those regions + */ FOREACH_HEAP_VAR(ctx, var) { if (var_owns_region(var) && var->init_attrs.has_region_offset) { pick_one(ctx, st, var, var_owned_region_size(var)); } } - /* pick the vars pinned to the same region as another */ + /* now pick any aliased ones */ FOREACH_HEAP_VAR(ctx, var) { - if (var->ty == VAR_PINNED) { - pick_one(ctx, st, var, var->heap.owned_region_size); + if (var->ty == VAR_ALIAS) { + /* TODO: BS: the alias is only a single page right now + * maybe in future we want it to be the same size as the .aliased_with var */ + pick_one(ctx, st, var, REGION_OWN_PAGE); } } - /* finally, pick any that remain */ - for (own_level_t lvl = REGION_OWN_PGD; lvl > REGION_OWN_VAR; lvl--) { - FOREACH_HEAP_VAR(ctx, var) { - if (! st->var_sts[var->varidx].picked) { - pick_one(ctx, st, var, lvl); - } - } + /* should be none left over */ + FOREACH_HEAP_VAR(ctx, var) { + fail_on (!st->var_sts[var->varidx].picked, "failed to pick a VA for \"%s\"\n", var->name); } + /* because we pick the owned regions at random, they may overlap + * so check for overlaps and explicitly discard if so. + */ FOREACH_HEAP_VAR(ctx, var) { if (! validate_selection(ctx, st, var)) { debug("for run #%ld failed to validate the picks, trying again...\n", run); diff --git a/lib/litmus_test/litmus_test_var_info.c b/lib/litmus_test/litmus_test_var_info.c index 4a580e0b..98b62084 100644 --- a/lib/litmus_test/litmus_test_var_info.c +++ b/lib/litmus_test/litmus_test_var_info.c @@ -90,19 +90,23 @@ void read_var_infos(const litmus_test_t* cfg, init_system_state_t* sys_st, var_i } } - /* for all variables without an explicit offset, make them offset from the primary var - * at the same page offset */ + /* for all variables without an explicit offset, + * and which aren't pinned to another, + * make them offset from the primary var + * at the same page offset + */ for (var_idx_t v = 0; v < cfg->no_heap_vars; v++) { var_info_t* vinfo = &infos[v]; if (vinfo->varidx == first->varidx) continue; + if (vinfo->ty == VAR_PINNED) + continue; + if (vinfo->init_attrs.has_region_offset) continue; - /* ensure all vars with no explicit INIT_REGION_OFFSET have the same offset in the owned region - */ vinfo->init_attrs.has_region_offset = 1; vinfo->init_attrs.region_offset.offset_var = first->varidx; vinfo->init_attrs.region_offset.offset_level = REGION_SAME_PAGE_OFFSET;