|Johan Janzén: Leveraging application diversity with GPU co-scheduling|
Location: ITC 1145, Time: 13:15-14:00
GPU as a compute platform has become ubiquitous in high performance computing today and more classes of algorithms are successfully moved to this platform. Algorithms and tasks that struggle to scale to the full GPU efficiently present an opportunity for co-scheduling. This challenge requires available knowledge about task scalability as well fast-enough re-allocation features, and has the potential of efficient use of GPUs in multi-appliation and virtual environments in the future. By profiling online and with careful dynamic reallocation of compute resources we show that we can harness application diversity for improved performance when available, while keeping the performance high when tasks already scale.
|Anke Stüber: Towards a framework of privacy notions for process algebra|
Location: ITC 1111, Time: 15:15
Nowadays, where even toasters are connected to the Internet, and
software routinely handles personal data, it has become important for
software developers to tackle the difficult problem of ensuring privacy
for their users. Process algebra gives us a tool to formally verify the
privacy properties of concurrent systems, but until recently there
existed no widely accepted formal definitions of privacy notions.
Authors differed slightly in how they translated informal descriptions
into formal definitions, making comparisons of their results difficult.
In 2019, Kuhn et al. presented a hierarchy of formal definitions of
privacy notions for anonymous communication networks, based on
indistinguishability games. In this seminar I will present a related
approach using process algebra, where behavioural equivalence tests are
used instead of indistinguishability games, and where it is clearly
defined which events are observable to an attacker. This formalisation
will further the understanding of privacy properties, and may lead to
the discovery of conditions that are sufficient to ensure certain
privacy notions while being automatically verifiable with existing
process algebra tools.
|Licentiatseminarium | Licentia|
|Huu-Phuc Vo: Towards Machine-Assisted Reformulation for MiniZinc|
Location: ITC 1213, Time: 15:15
Model reformulation plays an important role in improving models, reducing search space so that solutions can be found faster. Hence we categorise model reformulation into three types: a model is reformulated to another model with the same modelling language, a model with non constraint programming standard types is compiled to another model with constraint programming (CP) standard types, and a model is converted to Boolean satisfiability problem (SAT), Mixed-integer programming (MIP), Satisfiability modulo theories (SMT), and Mixed integer linear programming (MILP). Based on these categories, reformulation and compilation could be used in different ways to improve a model such as automatic reformulations, semiautomatic reformulations, MIP to constraint programming, implied constraints, set Constraint Satisfaction Problems (CSPs) to CSPs, string variables to CSP without string variables, symmetry breaking, pre-computation, non-binary to binary translations, and reformulations into SAT, MILP, and SMT. CP is a pervasive and highly successful technology for solving a wide variety of constraint satisfaction problems such as air traffic management, resource allocation, transportation, scheduling, and so on. Model reformulation can have a significant impact on solving time. Techniques from formal methods will be used to provide machine assistance for MiniZinc, which is the high-level modelling language to model CSPs. In this thesis, we present an overview of reformulation focusing on the contributions made in the area of reformulation of CSPs where significant performance improvements have been achieved. Our contributions are as follows: propose criteria and types that categorise model reformulations; we systematically unify and organise the vast literature; contrast and compare different categories of the reformulation for solving CSPs; propose a compiler for counter automata reformulation; ultimately, we propose a plan for future work, we identify the challenges, implement frameworks, and evaluate our experimental results of model reformulations.