Automated Correct Algorithm Transformation into Map Reduce
| Typ: | MA |
|---|---|
| Datum: | 2018-01-26 |
| Betreuer: | Mattias Ulbrich |
| Aushang: |
while / for ====> map / reduce
Today requirements on the efficiency and scale of computations grow faster than the capabilities of the hardware on which they are to run. Frameworks such as Map/Reduce that distribute the computation workload amongst many nodes in a cluster, address this challenges by providing a limited set of operations whose execution is automatically and transparently parallelized and distributed among the available nodes.
Formulating efficient implementations in such frameworks is a challenge in itself. The original algorithmic structure of a corresponding imperative algorithm is often lost during that translation since imperative constructs do not translate directly to the provided primitives.
This thesis contributes to providing a solution to this challenge!
Task
You implement a user-guided, automated translation framework which allows one to transform an imperative program into an equivalent Map/Reduce implementation.
You can build on existing work in which we identified transformation rules which are relevant for this task. Most of them have been formally proved correct.
A prototype of a manual proof system exists -- now it's time to automate the process.
Your profile
You are interested in formal systems and/or formal languages. You know how to implement smaller software systems (including parser etc). Knowledge as taught in the lecture Formale Methoden (or equivalent) is required.
Die Arbeit kann auf englisch oder deutsch betreut / verfasst werden.