Research Buffet
Friday, November 18, 2011
3147 MEB
Lecture 4:00 p.m.
Grant Ayers
Title: How to build your own message passing multicore starting from gates, and program it
Friday, November 18, 2011
3147 MEB
Lecture 4:00 p.m.
Grant Ayers
Title: How to build your own message passing multicore starting from gates, and program it
Abstract
The microprocessor industry has made a dramatic shift from single- to multi-core designs. However, the popularized version of Moore’s law which expects a doubling of performance every couple of years has ended. While transistor counts continue to increase, the lack of software and hardware models to properly and efficiently embrace the multicore paradigm has prevented us from seeing substantial performance gains.
My research with XUM (the eXtensible Utah Multicore project) has focused on developing an open hardware and software platform suitable for a wide range of multicore research. Its (presently 8x 32-bit MIPS core-based) hardware is designed from the ground up, and its open nature allows for arbitrary customization for various applications. In this talk, I will introduce the architecture of XUM and illustrate the pathway from hardware design to running programs generated from a C compiler. Acknowledgements: The initial version of XUM is due to Ben Meakin, former MS student.
Tyler Sorensen
Title: Using Logical Decision Procedures to Power Puzzle Solving Engines
The microprocessor industry has made a dramatic shift from single- to multi-core designs. However, the popularized version of Moore’s law which expects a doubling of performance every couple of years has ended. While transistor counts continue to increase, the lack of software and hardware models to properly and efficiently embrace the multicore paradigm has prevented us from seeing substantial performance gains.
My research with XUM (the eXtensible Utah Multicore project) has focused on developing an open hardware and software platform suitable for a wide range of multicore research. Its (presently 8x 32-bit MIPS core-based) hardware is designed from the ground up, and its open nature allows for arbitrary customization for various applications. In this talk, I will introduce the architecture of XUM and illustrate the pathway from hardware design to running programs generated from a C compiler. Acknowledgements: The initial version of XUM is due to Ben Meakin, former MS student.
Tyler Sorensen
Title: Using Logical Decision Procedures to Power Puzzle Solving Engines
Abstract
While many are aware of the deep connection between mathematical logic and computer science, there are very few elementary applications promoting this idea. Logic and arithmetic puzzles provide a simple framework for introducing this connection while still considering fundamental problems like NP-completeness and decidability. In this talk, I will show how to solve a puzzle by using mathematical logic to formulate constraints that can then be given to a decision engine. Furthermore, different background theories will be analyzed and considered for different puzzles.
I will present examples using two original tools: A ken-ken puzzle solver using Microsoft's Z3 (an SMT solver used for fuzz testing thousands of real-life applications) and a binary decision diagram generator implemented in Python for solving some interesting puzzles proposed by Lewis Carroll (logician, and author of Alice in Wonderland).
While many are aware of the deep connection between mathematical logic and computer science, there are very few elementary applications promoting this idea. Logic and arithmetic puzzles provide a simple framework for introducing this connection while still considering fundamental problems like NP-completeness and decidability. In this talk, I will show how to solve a puzzle by using mathematical logic to formulate constraints that can then be given to a decision engine. Furthermore, different background theories will be analyzed and considered for different puzzles.
I will present examples using two original tools: A ken-ken puzzle solver using Microsoft's Z3 (an SMT solver used for fuzz testing thousands of real-life applications) and a binary decision diagram generator implemented in Python for solving some interesting puzzles proposed by Lewis Carroll (logician, and author of Alice in Wonderland).