May 2015 - talks - lists.cs.princeton.edu

Heejin Ahn will present her general exam on May 21, 2015 at 1:30pm in CS 401.
by Nicki Gotsis 12 May '15

12 May '15

Heejin Ahn will present her general exam on May 21, 2015 at 1:30pm in CS 401. The members of her committee are: David August (adviser), Aarti Gupta, and Andrew Appel. Everyone is invited to attend her talk, and those faculty wishing to remain for the oral exam following are welcome to do so. Her abstract and reading list follow below. Program Approximation by Partial Loop Execution Many application domains, such as multimedia applications, simulations, and machine learning algorithms, allow opportunities to trade-off the quality of results for performance or energy improvements. Various compilation techniques have proposed to approximate program results in order to improve performance or reduce energy consumption. However, the applicability of previous work has been limited to DOALL-style loops with very regular structures. This work presents a compiler technique that transforms loops to skip parts of iterations even in the presence of loop-carried dependences or recursive data structure traversal. From a given loop iteration, we use compiler analysis to identify computations that are essential for the loop to continue, and skip or use memoized results for the remaining non-critical computations at a configured frequency. As a result, this work provides similar speedup with previous techniques while being applicable to a wider range of loops. >>> 1 Reading List >>> 1.1 Textbooks >>> • A. W. Appel. Modern Compiler Implementation in C. Cambridge University Press, 1998 >>> • J. L. Hennessy and D. A. Patterson. Computer Architecture: A Quantitative Approach, Fourth Edition. Morgan >>> Kaufmann, 2006 >>> 1.2 Software-only Approximation >>> • J. Liu, W.-K. Shih, K.-J. Lin, R. Bettati, and J.-Y. Chung. Imprecise computations. Proceedings of the IEEE, >>> 82(1):83–94, Jan 1994 >>> • M. Rinard. Probabilistic accuracy bounds for fault-tolerant computations that discard tasks. In Proceedings of >>> the 20th Annual International Conference on Supercomputing, ICS ’06, pages 324–334, New York, NY, USA, >>> 2006. ACM >>> • W. Baek and T. M. Chilimbi. Green: A framework for supporting energy-conscious programming using controlled >>> approximation. In Proceedings of the 31st ACM SIGPLAN Conference on Programming Language >>> Design and Implementation (PLDI), pages 198–209, 2010 >>> • S. Sidiroglou-Douskos, S. Misailovic, H. Hoffmann, and M. Rinard. Managing performance vs. accuracy tradeoffs >>> with loop perforation. In Proceedings of the 19th ACM SIGSOFT Symposium and the 13th European >>> Conference on Foundations of Software Engineering, ESEC/FSE ’11, pages 124–134, New York, NY, USA, >>> 2011. ACM >>> • S. Misailovic, D. Kim, and M. Rinard. Parallelizing sequential programs with statistical accuracy tests. ACM >>> Trans. Embed. Comput. Syst., 12(2s):88:1–88:26, May 2013 >>> • M. Samadi, D. A. Jamshidi, J. Lee, and S. Mahlke. Paraprox: Pattern-based approximation for data parallel >>> applications. In Proceedings of the 19th International Conference on Architectural Support for Programming >>> Languages and Operating Systems, ASPLOS ’14, pages 35–50, New York, NY, USA, 2014. ACM >>> • S. Campanoni, G. Holloway, G.-Y. Wei, and D. Brooks. Helix-up: Relaxing program semantics to unleash >>> parallelization. In Code Generation and Optimization (CGO), 2015 IEEE/ACM International Symposium on, >>> pages 235–245, Feb 2015 >>> 1.3 Approximation on Unreliable Hardware >>> • A. Sampson, W. Dietl, E. Fortuna, D. Gnanapragasam, L. Ceze, and D. Grossman. Enerj: Approximate data >>> types for safe and general low-power computation. In Proceedings of the 32Nd ACM SIGPLAN Conference on >>> Programming Language Design and Implementation, PLDI ’11, pages 164–174, New York, NY, USA, 2011. >>> ACM >>> • H. Esmaeilzadeh, A. Sampson, L. Ceze, and D. Burger. Neural acceleration for general-purpose approximate >>> programs. In Proceedings of the 2012 45th Annual IEEE/ACM International Symposium on Microarchitecture, >>> MICRO-45, pages 449–460, Washington, DC, USA, 2012. IEEE Computer Society >>> • J. Park, X. Zhang, K. Ni, H. Esmaeilzadeh, and M. Naik. Expax: A framework for automating approximate programming. >>> Technical report, College of Computing, Georgia Institute of Technology, North Ave NW, Atlanta, >>> GA 30332, USA, 2014 >>> References >>> [1] A. W. Appel. Modern Compiler Implementation in C. Cambridge University Press, 1998. >>> [2] W. Baek and T. M. Chilimbi. Green: A framework for supporting energy-conscious programming using controlled approximation. >>> In Proceedings of the 31st ACM SIGPLAN Conference on Programming Language Design and Implementation >>> (PLDI), pages 198–209, 2010. >>> [3] S. Campanoni, G. Holloway, G.-Y. Wei, and D. Brooks. Helix-up: Relaxing program semantics to unleash parallelization. In >>> Code Generation and Optimization (CGO), 2015 IEEE/ACM International Symposium on, pages 235–245, Feb 2015. >>> [4] H. Esmaeilzadeh, A. Sampson, L. Ceze, and D. Burger. Neural acceleration for general-purpose approximate programs. In >>> Proceedings of the 2012 45th Annual IEEE/ACM International Symposium on Microarchitecture, MICRO-45, pages 449–460, >>> Washington, DC, USA, 2012. IEEE Computer Society. >>> [5] J. L. Hennessy and D. A. Patterson. Computer Architecture: A Quantitative Approach, Fourth Edition. Morgan Kaufmann, >>> 2006. >>> [6] J. Liu, W.-K. Shih, K.-J. Lin, R. Bettati, and J.-Y. Chung. Imprecise computations. Proceedings of the IEEE, 82(1):83–94, >>> Jan 1994. >>> [7] S. Misailovic, D. Kim, and M. Rinard. Parallelizing sequential programs with statistical accuracy tests. ACM Trans. Embed. >>> Comput. Syst., 12(2s):88:1–88:26, May 2013. >>> [8] J. Park, X. Zhang, K. Ni, H. Esmaeilzadeh, and M. Naik. Expax: A framework for automating approximate programming. >>> Technical report, College of Computing, Georgia Institute of Technology, North Ave NW, Atlanta, GA 30332, USA, 2014. >>> [9] M. Rinard. Probabilistic accuracy bounds for fault-tolerant computations that discard tasks. In Proceedings of the 20th Annual >>> International Conference on Supercomputing, ICS ’06, pages 324–334, New York, NY, USA, 2006. ACM. >>> [10] M. Samadi, D. A. Jamshidi, J. Lee, and S. Mahlke. Paraprox: Pattern-based approximation for data parallel applications. >>> In Proceedings of the 19th International Conference on Architectural Support for Programming Languages and Operating >>> Systems, ASPLOS ’14, pages 35–50, New York, NY, USA, 2014. ACM. >>> [11] A. Sampson, W. Dietl, E. Fortuna, D. Gnanapragasam, L. Ceze, and D. Grossman. Enerj: Approximate data types for safe and >>> general low-power computation. In Proceedings of the 32Nd ACM SIGPLAN Conference on Programming Language Design >>> and Implementation, PLDI ’11, pages 164–174, New York, NY, USA, 2011. ACM. >>> [12] S. Sidiroglou-Douskos, S. Misailovic, H. Hoffmann, and M. Rinard. Managing performance vs. accuracy trade-offs with loop >>> perforation. In Proceedings of the 19th ACM SIGSOFT Symposium and the 13th European

1 0

1:30pm Fri May 15 talk by John Doyle (Caltech) on "Universal laws and architectures: Theory and lessons from brains, nets, hearts, bugs, grids, flows, and zombies"
by Jennifer Rexford 11 May '15

11 May '15

Speaker: John Doyle, Caltech Title: Universal laws and architectures: Theory and lessons from brains, nets, hearts, bugs, grids, flows, and zombies Date/time: 1:30-2:30pm Friday May 15 Location: CS 105 (small auditorium) Abstract: This talk aims to accessibly introduce a new theory of network architecture relevant to biology, medicine and technology (particularly SDN/NFV and cyberphysical systems), initially minimizing math details. Key ideas are motivated by familiar examples from neuroscience, including live demos using audience brains, and further illustrated with examples from technology and biology. The status of the necessary math will be sketched in as much detail as time permits. Background material is in online videos (accessible from website above) and a recent blog post: rigorandrelevance.wordpress.com/author/doyleatcaltech. My research is aimed at developing a more “unified” theory for complex networks motivated by and drawing lessons from neuroscience[4], cell biology[3], medical physiology[9], technology (internet, smartgrid, sustainable infrastructure)[1][8], and multiscale physics [2],[5],[6]. This theory involves several elements: hard limits, tradeoffs, and constraints on achievable robust, efficient performance ( “laws”), the organizing principles that succeed or fail in achieving them (“architectures” and protocols), the resulting high variability data and “robust yet fragile” behavior observed in real systems and case studies (behavior, data, statistics), the processes by which systems adapt and evolve (variation, selection, design), and their unavoidable fragilities (hijacking, parasites, predation, zombies). We will leverage a series of case studies with live demos from neuroscience, particularly vision and sensorimotor control, plus some hopefully familiar and simple insights from medicine, cell biology and modern computer and networking technology. Zombies emerge throughout as a ubiquitous, strangely popular, and annoying system fragility, particularly in the form of zombie science. In addition to the above mentioned blog and videos, papers [1] and [4] (and references therein) are the most accessible and broad introduction while the other papers give more domain specific details. For math details the best place to start is Nikolai Matni’s website (cds.caltech.edu/~nmatni/). Selected recent references: [1] Alderson DL, Doyle JC (2010) Contrasting views of complexity and their implications for network-centric infrastructures. IEEE Trans Systems Man Cybernetics—Part A: Syst Humans 40:839-852. [2] Sandberg H, Delvenne JC, Doyle JC. On Lossless Approximations, the Fluctuation-Dissipation Theorem, and Limitations of Measurements, IEEE Trans Auto Control, Feb 2011 [3] Chandra F, Buzi G, Doyle JC (2011) Glycolytic oscillations and limits on robust efficiency. Science, Vol 333, pp 187-192. [4] Doyle JC, Csete ME(2011) Architecture, Constraints, and Behavior, P Natl Acad Sci USA, vol. 108, Sup 3 15624-15630 [5] Gayme DF, McKeon BJ, Bamieh B, Papachristodoulou P, Doyle JC (2011) Amplification and Nonlinear Mechanisms in Plane Couette Flow, Physics of Fluids, V23, Issue 6, 065108 [6] Page, M. T., D. Alderson, and J. Doyle (2011), The magnitude distribution of earthquakes near Southern California faults, J. Geophys. Res., 116, B12309, doi:10.1029/2010JB007933. [7] Namas R, Zamora R, An, G, Doyle, J et al, (2012) Sepsis: Something old, something new, and a systems view, Journal Of Critical Care Volume: 27 Issue: 3 [8] Chen, L; Ho, T; Chiang, M, Low S; Doyle J,(2012) Congestion Control for Multicast Flows With Network Coding, IEEE Trans On Information Theory Volume: 58 Issue: 9 Pages: 5908-5921 [9] Li, Cruz, Chien, Sojoudi, Recht, Stone, Csete, Bahmiller, Doyle (2014) Robust efficiency Bio: John Doyle is the John G Braun Professor of Control & Dynamical Systems, Electrical Engineering, and BioEngineering at Caltech. His research interests are in theoretical foundations for complex networks in engineering and biology, as well as multiscale physics, and include integrating modeling, ID, analysis and design of uncertain nonlinear systems, and computation in analysis and simulation, including complexity theory to guide algorithm development. Research applications interests are motivated by the interplay between control, dynamical systems, and design and analysis of large, complex systems. His home page is http://www.cds.caltech.edu/~doyle

1 0

Steven Goldfeder will be presenting his generals May 18, 2015 at 10:15am in CS 401.
by Nicki Gotsis 11 May '15

11 May '15

Steven Goldfeder will be presenting his generals May 18, 2015 at 10:15am in CS 401. The members of his committee are: Arvind Narayanan (adviser), Ed Felten, and Andrea LaPaugh. Everyone is invited to attend his talk, and those faculty wishing to remain for the oral exam following are welcome to do so. His abstract and reading list follow below. Abstract: The Bitcoin ecosystem has suffered frequent thefts and losses affecting both businesses and individuals. Due to the irreversibility, automation, and pseudonymity of transactions, Bitcoin currently lacks support for the sophisticated internal control systems deployed by modern businesses to deter fraud. While Bitcoin’s built-in mutisignature feature can be used to split control over a Bitcoin wallet and achieve access control, we show that using multisignatures leads to serious privacy and anonymity losses. To address this problem, we present the first threshold signature scheme compatible with Bitcoin’s ECDSA signatures and show how distributed Bitcoin wallets can be built using this primitive. For businesses, we show how our distributed wallets can be used to systematically eliminate single points of failure at every stage of the flow of bitcoins through the system. For individuals, we design, implement, and evaluate a two-factor secure Bitcoin wallet. Reading List: Anderson, Ross. Security engineering. John Wiley & Sons, 2008. Chapters 2, 4, 7, 10. Bonneau, Joseph, Andrew Miller, Jeremy Clark, Arvind Narayanan, Joshua A. Kroll and Edward W. Felten. “Research Perspectives and Challenges for Bitcoin and Cryptocurrencies”. To appear in IEEE Security & Privacy, 2015. De Cristofaro, Emiliano, Honglu Du, Julien Freudiger, and Greg Norcie. “Two-Factor or not Two-Factor? A Comparative Usability Study of Two-Factor Authentication.” 8th NDSS Workshop on Usable Security (USEC), 2014. Goldwasser, Shafi. "Multi party computations: past and present." In Proceedings of the sixteenth annual ACM symposium on Principles of distributed computing, pp. 1-6. ACM, 1997. Katz, Jonathan, and Yehuda Lindell. Introduction to modern cryptography. CRC Press, 2014. Langford, Susan K. "Threshold DSS signatures without a trusted party." In Advances in Cryptology—CRYPT0’95, pp. 397-409. Springer Berlin Heidelberg, 1995. Lindell, Yehuda, and Benny Pinkas. "Secure multiparty computation for privacy-preserving data mining." Journal of Privacy and Confidentiality 1, no. 1 (2009): 5. Section 3: Constructions. MacKenzie, Philip, and Michael K. Reiter. "Two-party generation of DSA signatures." In Advances in Cryptology—CRYPTO 2001, pp. 137-154. Springer Berlin Heidelberg, 2001. Meiklejohn, Sarah, Marjori Pomarole, Grant Jordan, Kirill Levchenko, Damon McCoy, Geoffrey M. Voelker, and Stefan Savage. "A fistful of bitcoins: characterizing payments among men with no names." In Proceedings of the 2013 conference on Internet measurement conference, pp. 127-140. ACM, 2013. Moore, Tyler, and Nicolas Christin. "Beware the middleman: Empirical analysis of bitcoin-exchange risk." In Financial Cryptography and Data Security, pp. 25-33. Springer Berlin Heidelberg, 2013. Nakamoto, Satoshi. "Bitcoin: A peer-to-peer electronic cash system." Shamir, Adi. "How to share a secret." Communications of the ACM 22, no. 11 (1979): 612-613. Wu, Thomas, Michael Malkin, and Dan Boneh. "Building Intrusion Tolerant Applications." In Proceedings of the 8th USENIX Security Symposium, 1999.

1 0

Elba Garza will present her MSE thesis talk on May 12, 2015 at 1:30pm in CS 401.
by Nicki Gotsis 11 May '15

11 May '15

Elba Garza will present her MSE thesis talk on May 12, 2015 at 1:30pm in CS 401. The members of her committee are Margaret Martonosi, Doug Clark, and Kelly Shaw (University of Richmond). Everyone is invited to attend her talk. Her abstract follows below. Title: Efficient Design Space Exploration Techniques in Heterogeneous Systems Abstract: Heterogeneous architectures allow for computational offloading to various compute units such as graphics processing units (GPUs) and application-specific integrated circuits (ASICs). These compute units often require proper hardware and software parameter settings to reach power and performance goals. Optimization of these parameter setting configurations can be conducted through exploration of the parameters’ cumulative design space. Exhaustive exploration is often impractical or impossible due to spaces’ exponential growth with the addition of parameters. For example, a GPU design space analyzed in this work included 47 billion possible parameter set- ting configurations. Utilizing a statistical learning technique called Starchart, we have been able to optimize design space exploration for parameters in some heterogeneous architecture components. We extend Starchart to create Iterative Starchart, which allows non-uniform iterative sampling from certain parts of the design space. Iterative sampling allows the user to focus on areas of interest or importance to the space, whether it be due to performance measurements or necessary parameter constraints. This extension to Starchart results in efficient and tractable design space assessment. To show these properties, we apply Iterative Starchart to re-explore the real-data GPU design spaces from the original publication. We show Iterative Starchart ex- tends prediction performance accuracy by 21% in high-performance areas of interest. Furthermore, we explore design spaces of fixed-function accelerators simulated via, Aladdin, a power-performance simulator. In these accelerator spaces, Iterative Starchart extends prediction performance accuracy by 14% in high-performance areas of interest. These two test cases show Iterative Starchart ca be a valuable and powerful tool for exploring the design spaces of compute units in heterogeneous architectures.

1 0

Fwd: Today: EE Department Seminar-Pramod Viswanath-Spy vs Spy: Anonymous Messaging- 4:30pm E-Quad B2015
by Jennifer Rexford 08 May '15

08 May '15

> From: "Lisa R. Lewis" <ll2(a)Princeton.EDU> > Date: May 8, 2015 at 9:57:47 AM EDT > To: ee-seminar(a)Princeton.EDU > Subject: Today: EE Department Seminar-Pramod Viswanath-Spy vs Spy: Anonymous Messaging- 4:30pm E-Quad B2015 > Reply-To: "Lisa R. Lewis" <ll2(a)Princeton.EDU> > > TODAY: > > DEPARTMENT OF > ELECTRICAL ENGINEERING SEMINAR SERIES > > > Title: Spy vs Spy: Anonymous Messaging > Date: Friday, May 8, 2015 > Time: 4:30pm > Room: E-Quad, B205 > Host: Prateek Mittal > > Abstract: Anonymous messaging platforms, such as Secret, Whisper and Yik Yak, have emerged as important social media for sharing one's thoughts without the fear of being judged by friends, family, or the public. Further, such anonymous platforms are crucial in nations with authoritarian governments, where the right to free expression and, sometimes, the personal safety of the message author depends on anonymity. Current platforms offer only superficial anonymity -- their centralized implementation makes them naturally vulnerable to authoritarian adversaries and/or economic incentives. In this talk, we study the problem of designing a distributed messaging protocol that spreads the message fast while keeping the identity of the source hidden from an adversary. We present an anonymous messaging protocol, which we call adaptive diffusion (and is related to the Chinese restaurant process), and show that it spreads fast and achieves nearly perfect obfuscation of the source for a wide range of adversaries. System issues in the implementation of the protocol are discussed. > > Bio: Pramod Viswanath received the PhD degree in EECS from the University of California at Berkeley in 2000. He was a member of technical staff at Flarion Technologies until August 2001 before joining the ECE department at the University of Illinois, Urbana-Champaign. He is a recipient of the Xerox Award for Faculty Research from the College of Engineering at UIUC (2010), the Eliahu Jury Award from the EECS department of UC Berkeley (2000), the Bernard Friedman Award from the Mathematics department of UC Berkeley (2000), and the NSF CAREER Award (2003). He was an associate editor of the IEEE Transactions on Information Theory for the period 2006-2008. >

1 0

Qinxiang Cao will present his Generals on May 18, 2015 at 1:30PM in CS 302.
by Nicki Gotsis 07 May '15

07 May '15

Qinxiang Cao will present his Generals on May 18, 2015 at 1:30PM in CS 302. The members of his committee are as follows: Andrew Appel (adviser), Aarti Gupta, and David Walker. Abstract: Program Verification on Aggregate Types in C. Verifiable Software Toolchain (VST) is a verified tool to prove the full functional correctness of C programs. As introduced by Hoare logic, pre/post conditions are used in VST to specify program behaviors. And these specifications can be proved by applying Hoare rules. However, when aggregate C types are involved, pre/post conditions become messy. Users need to write (assertion) conjuncts for every field of a struct type in pre/post conditions. Since structs, unions and arrays can be nested together arbitrarily in C, this leads to very verbose assertions. In this work, we define a spatial predicate to describe aggregate-typed data more concisely. Then we define concise (derived) Hoare rules about loading/storing on aggregate data types. All these rules are compatible with the separation logic settings in VST. As our assertion predicate on aggregate types has to be dependently typed, we carefully designed the type system such that users do not need to worry about Coq's type checking issue. Text books: Michael Huth, Mark Ryan. Logic in Computer Scienc, Modelling and Reasoning about Systems. 2004. B. Pierce. Types and Programming Languages. 2002. Papers and Book Chapters: [Reynolds] J.C. Reynolds. Separation Logic: a Logic for Shared Mutable Data Structures. In LICS’02: Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science, pages 55 - 74, 2002. [Stephen Brookes] A semantics for concurrent separation logic. In Theoretical Computer Science, Volume 375, Issues 1–3, 1 May 2007, Pages 227–270 [Andrew W. Appel, Paul-André Melliès, Christopher D. Richards, Jérôme Vouillon] A very modal model of a modern, major, general type system. In POPL 20007. [A. W. Appel] VeriSmall: Veriﬁed Smallfoot Shape Analysis. In First International Conf. on Certiﬁed Programs and Proofs Dec. 2011 [Yves Bertot, Pierre Casteran] Interactive Theorem Prving and Program Development. Chapter 1 - Chapter 9. [Cristiano Calcagno, Dino Distefano Peter O’Hearn Hongseok Yang] Compositional Shape Analysis by means of Bi-Abduction [Dirk van Dalen] Intuitionistic Logic. In Logics and Structures, Chapter 5, 1994 [Ranjit Jhala, Rupak Majumdar] Software model checking. ACM Computing Surveys 41(4) (2009)

1 0

Kevin Lai will present his MSE thesis talk on Friday, May 8th, 2015 at 3pm in CS 302.
by Nicki Gotsis 06 May '15

06 May '15

Kevin Lai will present his MSE thesis talk on Friday, May 8th, 2015 at 3pm in CS 302. The members of his committee are: Moses Charikar (advisor) and Elad Hazan Everyone is invited to attend his talk. His abstract follows below. Title: Label optimal regret bounds for online local learning Abstract: In many settings, we would like to make predictions about the local structure of a problem rather than explicitly trying to learn some global structure. For instance, given two teams from some set of teams, we may want to know if one team will beat the other, while we may not be explicitly interested in a ranking of all of the teams. A recent framework proposed by Christiano 2014 called "online local learning'' captures this broad class of problems, which includes online max cut and online gambling. Christiano provides a Follow-the-Regularized-Leader algorithm using a log determinant regularizer to obtain low regret in this setting. In this work, we improve the analysis of Christiano's algorithm and present a matching lower bound based on a reduction from the planted clique problem, which is believed to have no polynomial-time algorithm for planted cliques of size k = o(n^(1/2)). Joint work with Pranjal Awasthi, Moses Charikar, and Andrej Risteski

1 0

Ryan Beckett will be presenting his Generals on May 15, 2015 at 2:30pm in CS 401.
by Nicki Gotsis 06 May '15

06 May '15

Ryan Beckett will be presenting his Generals on May 15, 2015 at 2:30pm in CS 401. The members of his committee are as follows: David Walker (advisor), Aarti Gupta, and Andrew Appel. Everyone is invited to attend his talk, and those faculty wishing to remain for the oral exam following are welcome to do so. His abstract and reading list follow below. Abstract: Kleene algebra with tests (KAT) is a well-studied algebraic structure consisting of a Kleene Algebra with an embedded Boolean subalgebra. KAT has been applied to a wide variety of equational program specification and verification tasks including communication protocols, static program analysis, lazy caching, concurrency control, and compiler optimizations. NetKAT, a KAT for defining network policies, has recently garnered much attention for its utility in both programming networks and verifying network program equivalence. We formalize an algebraic extension to NetKAT by lifting its Boolean subalgebra to a more expressive past-time linear temporal logic with tests ranging over packet history. Temporal logic tests enable the modular specification of networking properties such as reachability and waypointing, the construction of queries for network monitoring and debugging, and the concise description of programs using history-based routing. We develop an equational theory for NetKAT with an embedded temporal logic and prove that the equational theory is both sound and complete with respect to the denotational semantics. We conclude by discussing the broader applicability of our approach to KAT in general. Books: B. Pierce, Types and programming languages. MIT Press, 2002. (chapters 1-17, 20-25) M. Huth and M. Ryan, Logic in computer science, 2nd ed. Cambridge University Press, 2000. (chapters 1-5) D. Harel, D. Kozen and J. Tiuryn, Dynamic logic. MIT Press, 2000. (chapter 5) Papers: R. Jhala and R. Majumdar. Software model checking. ACM Comput. Surv., 41(4):1–54, 2009. L. Zhang and S. Malik. The quest for efficient boolean satisfiability solvers. In CAV, 2002. J. Desharnais, B. Moller and G. Struth. Modal Kleene algebra and applications: a survey. Relational Methods in Computer Science, 1:93–131, 2004. A. Greenburg et al. A clean slate 4D approach to network control and management. In SIGCOMM, 2005. P. Kazemian, G. Varghese and N. McKeown. Header space analysis: static checking for networks. In NSDI, 2012. S. Basu et al. Merlin: a language for provisioning network resources. In CoNEXT, 2014. C. Monsanto et al. A compiler and run-time system for network programming languages. In POPL, 2012. C. Anderson et al. NetKAT: semantic foundations for networks. In POPL, 2014. N. Foster et al. A coalgebraic decision procedure for NetKAT. In POPL, 2015.

1 0

Jennifer Gossels will be presenting her Generals on May 14, 2015 at 2pm in CS 402.
by Nicki Gotsis 06 May '15

06 May '15

Jennifer Gossels will be presenting her Generals on May 14, 2015 at 2pm in CS 402. The members of her committee are Jennifer Rexford (adviser), David Walker, and JP Singh. Everyone is invited to attend her talk, and those faculty wishing to remain for the oral exam following are welcome to do so. Her abstract and reading list follow below. Topology Virtualization in Software Defined Networks Software defined networking (SDN) is a promising tool that we can use to improve network performance and simplify network management. SDN is based on the concepts of (1) separation of the data and control planes through an open interface to switch hardware; and (2) logically centralized control. Nevertheless, SDN by itself is not a panacea; we need higher-level abstractions and support for modularity on top of OpenFlow, the industry standard interface between switches and controller. Our work achieves these goals by abstracting a single physical switch into a multi-switch virtual network. With this one-physical-to-many-virtual topology virtualization, administrators can run a combination of off-the-shelf controller applications, each of which relies on its own assumptions about the physical network. In contrast, without virtualization the administrator would need to implement his entire high-level policy in a custom, monolithic application tailored to his physical infrastructure. Further, topology virtualization enhances security by hiding the details of the physical network from third-party applications. In this talk we discuss the challenges of supporting the one-physical-to-many-virtual topology abstraction in SDNs, and then we describe our solutions to these problems. We begin with a precise definition of what it means to correctly implement this abstraction. Then, we present algorithms for translating controller-to-switch messages and switch-to-controller events both correctly and efficiently. We also discuss our implementation of some of these algorithms in our prototype network hypervisor and evaluate their overhead. This work builds on earlier research with Xin Jin, Jennifer Rexford, and David Walker presented at NSDI 2015 [6]. [1] Casado, M., Freedman, M. J., Pettit, J., Luo, J., McKeown, N., and Shenker, S. Ethane: Taking Control of the Enterprise. In Proceedings of the 2007 Conference on Applications, Technologies, Architectures, and Protocols for Computer Communications (New York, NY, USA, 2007), SIGCOMM ’07, ACM. [2] Clark, D. The Design Philosophy of the DARPA Internet Protocols. SIGCOMM Computer Communication Review 18, 4 (August 1988). [3] Ghorbani, S., and Godfrey, B. Towards Correct Network Virtualization. In Proceedings of the Third Workshop on Hot Topics in Software Defined Networking (New York, NY, USA, 2014), HotSDN ’14, ACM. [4] Ghorbani, S., Schlesinger, C., Monaco, M., Keller, E., Caesar, M., Rexford, J., and Walker, D. Transparent, Live Migration of a Software-Defined Network. In Proceedings of the ACM Symposium on Cloud Computing (New York, NY, USA, 2014), SOCC ’14, ACM. [5] Gupta, A., Vanbever, L., Shahbaz, M., Donovan, S. P., Schlinker, B., Feamster, N., Rexford, J., Shenker, S., Clark, R. J., and Katz-Bassett, E. SDX: A Software Defined Internet Exchange. In ACM SIGCOMM 2014 Conference, SIGCOMM ’14, Chicago, IL, USA, August 17-22, 2014 (2014). [6] Jin, X., Gossels, J., Rexford, J., and Walker, D. CoVisor: A Compositional Hypervisor for Software-Defined Networks. In Proceedings of the 12th USENIX Conference on Networked Systems Design and Implementation (May 2015), NSDI ’15. [7] Katta, N., Alipourfard, O., Rexford, J., and Walker, D. Infinite CacheFlow in Software-Defined Networks. In Proceedings of the Third Workshop on Hot Topics in Software Defined Networking (New York, NY, USA, 2014), HotSDN ’14, ACM. [8] Kazemian, P., Chang, M., Zeng, H., Varghese, G., McKeown, N., and Whyte, S. Real Time Network Policy Checking Using Header Space Analysis. In Proceedings of the 10th USENIX Conference on Networked Systems Design and Implementation (Berkeley, CA, USA, 2013), NSDI ’13, USENIX Association. [9] Koponen, T., Amidon, K., Balland, P., Casado, M., Chanda, A., Fulton, B., Ganichev, I., Gross, J., Gude, N., Ingram, P., Jackson, E., Lambeth, A., Lenglet, R., Li, S.-H., Padmanabhan, A., Pettit, J., Pfaff, B., Ramanathan, R., Shenker, S., Shieh, A., Stribling, J., Thakkar, P., Wendlandt, D., Yip, A., and Zhang, R. Network Virtualization in Multitenant Datacenters. In Proceedings of the 11th USENIX Conference on Networked Systems Design and Implementation (Berkeley, CA, USA, 2014), NSDI’14, USENIX Association, pp. 203–216. [10] Monsanto, C., Reich, J., Foster, N., Rexford, J., and Walker, D. Composing Software Defined Networks. In Proceedings of the 10th USENIX Conference on Networked Systems Design and Implementation (Berkeley, CA, USA, 2013), NSDI ’13, USENIX Association. [11] Peterson, L. L., and Davie, B. S. Computer Networks, Fifth Edition: A Systems Approach, 5th ed. Morgan Kaufmann Publishers Inc., San Francisco, CA, USA, 2011. [12] Sherwood, R., Gibb, G., Yap, K.-K., Appenzeller, G., Casado, M., McKeown, N., and Parulkar, G. Can the Production Network be the Testbed? In Proceedings of the 9th USENIX Conference on Operating Systems Design and Implementation (Berkeley, CA, USA, 2010), OSDI ’10, USENIX Association

1 0

Peng Sun will present his FPO on Wednesday, 5/13/2015 at 10am in CS 302.
by Nicki Gotsis 05 May '15

05 May '15

Peng Sun will present his FPO, "Integrating Network Management for Cloud Computing Services", on Wednesday, 5/13/2015 at 10am in CS 302. The members of his committee are: Jennifer Rexford (adviser), Readers: David Walker and Nick Feamster; Examiners: Margaret Martonosi, Kai Li, and Jennifer Rexford. A copy of his thesis, is available in Room 310. Everyone is invited to attend his talk.

1 0