Vous avez reçu un message "Your GitLab account has been locked ..." ? Pas d'inquiétude : lisez cet article https://docs.gricad-pages.univ-grenoble-alpes.fr/help/unlock/

Commit d4d8549c authored by Valentin Touzeau's avatar Valentin Touzeau Committed by Valentin Touzeau
Browse files

Initial commit

parents
CMAKE_MINIMUM_REQUIRED(VERSION 2.6)
# configuration
set(PLUGIN "lrumc") # plugin name
set(NAMESPACE "") # namespace
set(SOURCES "src/lrumc/lrumc.cpp"
"src/lrumc/MC/lrumc_MCProgramModelBuilding.cpp"
"src/lrumc/MC/lrumc_MCProgramModelSlicing.cpp"
"src/lrumc/MC/lrumc_MCProgramModelNode.cpp"
"src/lrumc/MC/lrumc_MCProgramModel.cpp"
"src/lrumc/MC/lrumc_MCCacheModel.cpp"
"src/lrumc/MC/lrumc_MCException.cpp"
"src/lrumc/MC/lrumc_MCNuxmvCommand.cpp"
"src/lrumc/MC/lrumc_MCInstance.cpp"
"src/lrumc/MC/lrumc_MCAnalysis.cpp"
"src/lrumc/MC/lrumc_MCQueryManager.cpp"
"src/lrumc/EM/lrumc_ExistMissDomain.cpp"
"src/lrumc/EM/lrumc_ExistMissAdapter.cpp"
"src/lrumc/EM/lrumc_ExistMissAnalysis.cpp"
"src/lrumc/EH/lrumc_ExistHitDomain.cpp"
"src/lrumc/EH/lrumc_ExistHitAdapter.cpp"
"src/lrumc/EH/lrumc_ExistHitAnalysis.cpp"
"src/lrumc/lrumc_ACSManager.cpp"
"src/lrumc/lrumc_DUCatBuilder.cpp"
)
# script
project(${PLUGIN})
# look for OTAWA
if(NOT OTAWA_CONFIG)
find_program(OTAWA_CONFIG otawa-config DOC "path to otawa-config")
if(NOT OTAWA_CONFIG)
message(FATAL_ERROR "ERROR: otawa-config is required !")
endif()
endif()
message(STATUS "otawa-config found at ${OTAWA_CONFIG}")
execute_process(COMMAND "${OTAWA_CONFIG}" --cflags OUTPUT_VARIABLE OTAWA_CFLAGS OUTPUT_STRIP_TRAILING_WHITESPACE)
execute_process(COMMAND "${OTAWA_CONFIG}" --libs --make-plug ${PLUGIN} -r OUTPUT_VARIABLE OTAWA_LDFLAGS OUTPUT_STRIP_TRAILING_WHITESPACE)
execute_process(COMMAND "${OTAWA_CONFIG}" --prefix OUTPUT_VARIABLE OTAWA_PREFIX OUTPUT_STRIP_TRAILING_WHITESPACE)
# plugin definition
set(ORIGIN $ORIGIN)
include_directories("${CMAKE_SOURCE_DIR}" "include")
add_library(${PLUGIN} SHARED ${SOURCES})
set_property(TARGET ${PLUGIN} PROPERTY PREFIX "")
set_property(TARGET ${PLUGIN} PROPERTY COMPILE_FLAGS "${OTAWA_CFLAGS} --std=c++11 -g -Wall -Wextra")
target_link_libraries(${PLUGIN} "${OTAWA_LDFLAGS}")
# installation
set(PLUGIN_PATH "${OTAWA_PREFIX}/lib/otawa/${NAMESPACE}")
install(TARGETS ${PLUGIN} LIBRARY DESTINATION ${PLUGIN_PATH})
install(FILES ${PLUGIN}.eld DESTINATION ${PLUGIN_PATH})
#ifndef LRUMC_ACS_MANAGER_H_
#define LRUMC_ACS_MANAGER_H_
#include <otawa/icat3/features.h>
#include <otawa/cfg/features.h>
namespace lrumc
{
class CacheState;
class ACSManager
{
public:
ACSManager(otawa::WorkSpace* ws);
~ACSManager(void);
void start(otawa::Block* b);
void update(const otawa::icache::Access& acc);
int mustAge(const otawa::icat3::LBlock* b);
int mayAge(const otawa::icat3::LBlock* b);
int existHitAge(const otawa::icat3::LBlock* b);
int existMissAge(const otawa::icat3::LBlock* b);
void print(const otawa::icat3::LBlock* b, otawa::io::Output& out);
private:
CacheState& use(int set);
otawa::icat3::ACSManager _underlyingManager;
const otawa::icat3::LBlockCollection& _coll;
elm::Vector<int> _used;
otawa::Block* _b;
CacheState** _states;
bool _hasExistHit;
bool _hasExistMiss;
};
} // namespace lrumc
#endif // LRUMC_ACS_MANAGER_H_
#ifndef LRUMC_EXIST_HIT_DOMAIN_H_
#define LRUMC_EXIST_HIT_DOMAIN_H_
#include <elm/io/Output.h>
#include <otawa/hard/Cache.h>
#include <otawa/icat3/features.h>
#include <otawa/icache/features.h>
#include <otawa/cfg/BasicBlock.h>
namespace lrumc {
class ExistHitDomain {
public:
using t = otawa::icat3::ACS;
ExistHitDomain(
const otawa::icat3::LBlockCollection& coll,
int set,
const t *init);
t init();
t bot();
void copy(t& d, const t& s);
t join(const t& d1, const t& d2);
bool equals(const t& v1, const t& v2);
void set(t& d, const t& s);
void dump(elm::io::Output& out, t c);
void update(otawa::Block *bb, t& a);
void update(otawa::Edge *e, t& a);
private:
void fetch(t& a, const otawa::icat3::LBlock *lb);
void update(const otawa::Bag<otawa::icache::Access>& os, t& a);
void update(const otawa::icache::Access& o, t& a);
const int _count;
const int _ways;
const t _bot, _top;
const t& _init;
otawa::hard::Cache::set_t _set;
const otawa::icat3::LBlockCollection& _coll;
};
} // namespace lrumc
#endif // LRUMC_EXIST_HIT_DOMAIN_H_
#ifndef LRUMC_FEATURES_H_
#define LRUMC_FEATURES_H_
#include <string>
#include <otawa/proc/AbstractFeature.h>
#include <otawa/icat3/features.h>
namespace lrumc {
// Exist-Hit
extern otawa::p::feature EXIST_HIT_ANALYSIS_FEATURE;
extern otawa::p::id<otawa::icat3::Container<otawa::icat3::ACS> > EXIST_HIT_INIT;
extern otawa::p::id<otawa::icat3::Container<otawa::icat3::ACS> > EXIST_HIT_IN;
// Exist-Miss
extern otawa::p::feature EXIST_MISS_ANALYSIS_FEATURE;
extern otawa::p::id<otawa::icat3::Container<otawa::icat3::ACS> > EXIST_MISS_INIT;
extern otawa::p::id<otawa::icat3::Container<otawa::icat3::ACS> > EXIST_MISS_IN;
// Definitely Unknown
enum class DUCategory
{
NC,
EH,
EM,
DU
};
extern otawa::p::feature DU_CATEGORY_FEATURE;
extern otawa::p::id<DUCategory> DU_CATEGORY;
// Model Checking
enum class CacheModelKind
{
YOUNGER_SET,
YOUNGER_SET_BITVECTOR,
YOUNGER_SET_CLOSED_BITVECTOR,
MAP_BLOCK_AGE,
QUEUE
};
enum class ProgramSlicing
{
SET_SLICING,
CACHE_BLOCK_SLICING,
ACCESS_SLICING
};
extern otawa::p::feature MODEL_CHECKING_ANALYSIS_FEATURE;
extern otawa::p::id<CacheModelKind> CACHE_MODEL_KIND;
extern otawa::p::id<ProgramSlicing> PROGRAM_SLICING;
extern otawa::p::id<elm::String> NUXMV_PATH;
extern otawa::p::id<elm::String> NUXMV_WORKSPACE_PATH;
} // namespace lrumc
namespace otawa
{
template <> void from_string(const elm::string& s, lrumc::CacheModelKind& v);
template <> void from_string(const elm::string& s, lrumc::ProgramSlicing& v);
} // namespace otawa
#endif // LRUMC_FEATURES_H
[elm-plugin]
name=lrumc
deps=otawa/icat3
description=Refine the May/Must classification of LRU cache blocks using Model Checking
author=Valentin Touzeau
#ifndef LRUMC_CACHE_STATE_H_
#define LRUMC_CACHE_STATE_H_
#include "EH/ExistHitDomain.h"
#include "EM/ExistMissDomain.h"
namespace lrumc
{
class CacheState
{
public:
CacheState(const otawa::icat3::LBlockCollection& coll, int set) :
_existHitDomain(coll, set, nullptr),
_existMissDomain(coll, set, nullptr),
_existHitState(nullptr),
_existMissState(nullptr)
{
}
~CacheState()
{
if(_existHitState)
delete _existHitState;
if(_existMissState)
delete _existMissState;
}
ExistHitDomain _existHitDomain;
ExistMissDomain _existMissDomain;
typename ExistHitDomain::t* _existHitState;
typename ExistMissDomain::t* _existMissState;
};
} // namespace lrumc
#endif // LRUMC_CACHE_STATE_H_
#ifndef LRUMC_EXIST_HIT_ADAPTER_H_
#define LRUMC_EXIST_HIT_ADAPTER_H_
#include <otawa/ai/ArrayStore.h>
#include <otawa/ai/TransparentCFGCollectionGraph.h>
#include <otawa/icat3/features.h>
#include <otawa/cfg/features.h>
#include "ExistHitDomain.h"
namespace lrumc
{
class ExistHitAdapter
{
public:
using domain_t = ExistHitDomain;
using t = typename domain_t::t;
using graph_t = otawa::ai::TransparentCFGCollectionGraph;
using store_t = otawa::ai::ArrayStore<domain_t, graph_t>;
ExistHitAdapter(int set, const t* init, const otawa::icat3::LBlockCollection& coll, const otawa::CFGCollection& cfgs, otawa::WorkSpace* ws);
inline domain_t& domain(void) { return _domain; }
inline graph_t& graph(void) { return _graph; }
inline store_t& store(void) { return _store; }
void update(const otawa::Bag<otawa::icache::Access>& accs, t& d);
void update(otawa::Block *v, t& d);
private:
otawa::icat3::ACSManager _mustManager;
domain_t _domain;
graph_t _graph;
store_t _store;
};
} // namespace lrumc
#endif // LRUMC_EXIST_HIT_ADAPTER_H_
#ifndef LRUMC_EXIST_HIT_ANALYSIS_H_
#define LRUMC_EXIST_HIT_ANALYSIS_H_
#include <otawa/proc/Processor.h>
#include <otawa/icat3/features.h>
#include <otawa/cfg/features.h>
namespace lrumc
{
class ExistHitAnalysis: public otawa::Processor
{
public:
static otawa::p::declare reg;
ExistHitAnalysis(otawa::p::declare& r = reg);
protected:
void configure(const otawa::PropList& props) override;
void setup(otawa::WorkSpace* ws) override;
void processWorkSpace(otawa::WorkSpace* ws) override;
void destroy(otawa::WorkSpace* ws) override;
private:
void processSet(int i, otawa::WorkSpace* ws);
const otawa::icat3::Container<otawa::icat3::ACS>* _initExistHit;
const otawa::icat3::LBlockCollection* _coll;
const otawa::CFGCollection* _cfgs;
};
/**
* Perform the ACS analysis for the Exist-Hit domain. For cache block, it associates an upper bound on block age that holds on at least on path
* @par Properties
* @li @ref EXIST_HIT_IN
*
* @par Configuraiton
* @li @ref EXIST_HIT_INIT
*
* @par Implementation
* @li @ref ExistHitAnalysis
*
* @ingroup lrumc
*/
extern otawa::p::feature EXIST_HIT_ANALYSIS_FEATURE;
/**
* ACS for the Exist-Hit analysis at the entry of the corresponding block or edge.
*
* @par Feature
* @li @ref EXIST_HIT_ANALYSIS_FEATURE
*
* @par Hooks
* @li @ref Block
* @li @ref Edge
*
* @ingroup lrumc
*/
extern otawa::p::id<otawa::icat3::Container<otawa::icat3::ACS> > EXIST_HIT_IN;
/**
* Initial state for Exist-Miss instruction cache analysis.
*
* @par Hook
* @li Feature configuration.
*
* @par Feature
* @li @ref EXIST_HIT_ANALYSIS_FEATURE
*
* @ingroup lrumc
*/
extern otawa::p::id<otawa::icat3::Container<otawa::icat3::ACS> > EXIST_HIT_INIT;
}; // namespace lrumc
#endif // LRUMC_EXIST_HIT_ANALYSIS_H_
#ifndef LRUMC_EXIST_HIT_DOMAIN_H_
#define LRUMC_EXIST_HIT_DOMAIN_H_
#include <otawa/icat3/features.h>
#include <otawa/icache/features.h>
namespace lrumc
{
class ExistHitDomain {
public:
using t = otawa::icat3::ACS;
ExistHitDomain(const otawa::icat3::LBlockCollection& coll, int set, const t* init);
inline const t& bot(void) const { return _bot; }
inline const t& top(void) const { return _top; }
inline const t& init(void) const { return _init; }
inline void print(const t& a, otawa::io::Output& out) const { a.print(_set, _coll, out); }
inline bool contains(const t& a, int i) { return(a[i] != otawa::icat3::BOT_AGE); }
inline void copy(t& d, const t& s) { d.copy(s); }
bool equals(const t& a, const t& b) const;
void join(t& d, const t& s);
void fetch(t& a, const otawa::icat3::LBlock *lb, otawa::icat3::ACSManager& mayManager);
void update(const otawa::icache::Access& access, t& a, otawa::icat3::ACSManager& mayManager);
private:
int _n;
t _bot, _top;
otawa::hard::Cache::set_t _set;
const otawa::icat3::LBlockCollection& _coll;
int _A;
const t& _init;
t _tmp;
};
} // namespace lrumc
#endif // LRUMC_EXIST_HIT_DOMAIN_H_
#include "ExistHitAdapter.h"
using namespace otawa;
namespace lrumc
{
ExistHitAdapter::ExistHitAdapter(
int set,
const t* init,
const icat3::LBlockCollection& coll,
const CFGCollection& cfgs,
otawa::WorkSpace* ws) :
_mustManager(ws),
_domain(coll, set, init),
_graph(cfgs),
_store(_domain, _graph)
{
}
void ExistHitAdapter::update(const Bag<icache::Access>& accs, t& d)
{
for(int i = 0; i < accs.count(); i++) {
_domain.update(accs[i], d, _mustManager);
_mustManager.update(accs[i]);
}
}
void ExistHitAdapter::update(Block *v, t& d)
{
cout << "Exist-Hit update\n";
_domain.copy(d, _domain.bot());
t s;
// update and join along edges
for(auto e = _graph.preds(v); e; e++) {
Block *w = e->source();
_domain.copy(s, _store.get(w));
_mustManager.start(v);
// apply block
{
const Bag<icache::Access>& accs = icache::ACCESSES(w);
if(accs.count() > 0)
update(accs, s);
}
// apply edge
{
const Bag<icache::Access>& accs = icache::ACCESSES(e);
if(accs.count() > 0)
update(accs, s);
}
// merge result
_domain.join(d, s);
cout << "\nnew value:\t";
_domain.print(d, cout);
cout << "\n";
}
}
} // namespace lrumc
#include "ExistHitAnalysis.h"
#include <otawa/ai/ArrayStore.h>
#include <otawa/ai/TransparentCFGCollectionGraph.h>
#include <otawa/ai/SimpleAI.h>
#include <otawa/icache/features.h>
#include <otawa/icat3/features.h>
#include <lrumc/features.h>
#include "ExistHitAdapter.h"
#include "ExistHitDomain.h"
using namespace otawa;
namespace lrumc
{
ExistHitAnalysis::ExistHitAnalysis(p::declare& r) :
Processor(r),
_initExistHit(nullptr),
_coll(nullptr),
_cfgs(nullptr)
{
}
void ExistHitAnalysis::configure(const PropList& props)
{
Processor::configure(props);
if(props.hasProp(EXIST_HIT_INIT))
_initExistHit = &EXIST_HIT_INIT(props);
}
void ExistHitAnalysis::setup(WorkSpace* ws)
{
_coll = icat3::LBLOCKS(ws);
ASSERT(_coll != nullptr);
_cfgs = INVOLVED_CFGS(ws);
ASSERT(_cfgs != nullptr);
}
void ExistHitAnalysis::processWorkSpace(WorkSpace* ws)
{
// prepare containers
for(CFGCollection::BlockIter b(_cfgs); b; b++)
(*EXIST_HIT_IN(b)).configure(*_coll);
// compute ACS
for(int i = 0; i < _coll->cache()->setCount(); i++) {
if((*_coll)[i].count()) {
if(logFor(LOG_FUN))
log << "\tanalyzing set " << i << io::endl;
processSet(i, ws);
}
}
}
void ExistHitAnalysis::destroy(WorkSpace*)
{
for(CFGCollection::BlockIter b(_cfgs); b; b++)
EXIST_HIT_IN(b).remove();
}
void ExistHitAnalysis::processSet(int i, WorkSpace* ws)
{
// perform the analysis
ExistHitAdapter ada(i, nullptr, *_coll, *_cfgs, ws);
ai::SimpleAI<ExistHitAdapter> ana(ada);
ana.run();
// store the results
for(CFGCollection::BlockIter b(_cfgs); b; b++)
if(b->isBasic()) {
ada.domain().copy((*EXIST_HIT_IN(b))[i], ada.store().get(b));
if(logFor(LOG_BLOCK))
log << "\t\t\t" << *b << ": " << ada.store().get(b) << io::endl;
}
}
p::declare ExistHitAnalysis::reg = p::init("lrumc::ExistHitAnalysis", Version(1, 0, 0))
.require(icat3::LBLOCKS_FEATURE)
.require(COLLECTED_CFG_FEATURE)
.require(icat3::MUST_PERS_ANALYSIS_FEATURE)
.provide(EXIST_HIT_ANALYSIS_FEATURE)
.make<ExistHitAnalysis>();
p::feature EXIST_HIT_ANALYSIS_FEATURE("lrumc::EXIST_HIT_ANALYSIS_FEATURE", p::make<ExistHitAnalysis>());
p::id<icat3::Container<icat3::ACS> > EXIST_HIT_IN("lrumc::EXIST_HIT_IN");
p::id<icat3::Container<icat3::ACS> > EXIST_HIT_INIT("lrumc::EXIST_HIT_INIT");
}; // namespace lrumc
#include "ExistHitDomain.h"
using namespace otawa;
namespace lrumc
{
ExistHitDomain::ExistHitDomain(
const icat3::LBlockCollection& coll,
int set,
const t *init) :
_n(coll[set].count()),
_bot(_n, icat3::BOT_AGE),
_top(_n, 0),
_set(set),
_coll(coll),
_A(coll.A()),
_init(init ? *init : _top),
_tmp(_n)
{
}
bool ExistHitDomain::equals(const t& a, const t& b) const
{
for(int i = 0; i < _n; i++)
if(a[i] != b[i])