- talks - lists.cs.princeton.edu

Kaiyu Yang will present his General Exam on Monday, January 20, 2020 at 1:30pm in CS 402.
by Nicki Mahler 13 Jan '20

13 Jan '20

Kaiyu Yang will present his General Exam on Monday, January 20, 2020 at 1:30pm in CS 402. The members of his committee are as follows: Jia Deng (adviser), Szymon Rusinkiewicz, and Olga Russakovsky 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. Title: SpatialSense: An Adversarially Crowdsourced Benchmark for Spatial Relation Recognition Abstract: Understanding the spatial relations between objects in images is a surprisingly challenging task. A chair may be "behind" a person even if it appears to the left of the person in the image (depending on which way the person is facing). Two students that appear close to each other in the image may not in fact be "next to" each other if there is a third student between them. We introduce SpatialSense, a dataset specializing in spatial relation recognition which captures a broad spectrum of such challenges, allowing for proper benchmarking of computer vision techniques. SpatialSense is constructed through adversarial crowdsourcing, in which human annotators are tasked with finding spatial relations that are difficult to predict using simple cues such as 2D spatial configuration or language priors. Adversarial crowdsourcing significantly reduces dataset bias and samples more interesting relations in the long tail compared to existing datasets. On SpatialSense, state-of-the-art recognition models perform comparably to simple baselines, suggesting that they rely on straightforward cues instead of fully reasoning about this complex task. The SpatialSense benchmark provides a path forward to advancing the spatial reasoning capabilities of computer vision systems. Textbook: [1] Szeliski, Richard. Computer vision: algorithms and applications . Springer Science & Business Media, 2010. Papers: [2] Krishna, Ranjay, et al. "Visual genome: Connecting language and vision using crowdsourced dense image annotations." International Journal of Computer Vision 123.1 (2017): 32-73. [3] Kuznetsova, Alina, et al. "The open images dataset v4: Unified image classification, object detection, and visual relationship detection at scale." arXiv preprint arXiv:1811.00982 (2018). [4] Lu, Cewu, et al. "Visual relationship detection with language priors." European Conference on Computer Vision . Springer, Cham, 2016. [4] Torralba, Antonio, and Alexei A. Efros. "Unbiased look at dataset bias." CVPR . Vol. 1. No. 2. 2011. [5] Sadeghi, Mohammad Amin, and Ali Farhadi. "Recognition using visual phrases." CVPR 2011 . IEEE, 2011. [6] Dai, Bo, Yuqi Zhang, and Dahua Lin. "Detecting visual relationships with deep relational networks." Proceedings of the IEEE Conference on Computer Vision and Pattern Recognition . 2017. [7] Xu, Danfei, et al. "Scene graph generation by iterative message passing." Proceedings of the IEEE Conference on Computer Vision and Pattern Recognition . 2017. [8] Peyre, Julia, et al. "Weakly-supervised learning of visual relations." Proceedings of the IEEE International Conference on Computer Vision . 2017. [9] Goyal, Yash, et al. "Making the V in VQA matter: Elevating the role of image understanding in Visual Question Answering." Proceedings of the IEEE Conference on Computer Vision and Pattern Recognition . 2017. [10] Zhang, Peng, et al. "Yin and yang: Balancing and answering binary visual questions." Proceedings of the IEEE Conference on Computer Vision and Pattern Recognition . 2016. [11] Attenberg, Josh M., Pagagiotis G. Ipeirotis, and Foster Provost. "Beat the machine: Challenging workers to find the unknown unknowns." Workshops at the Twenty-Fifth AAAI Conference on Artificial Intelligence . 2011.

1 0

Teague Tomesh will present his General Exam, "Minimizing State Preparations in Variational Quantum Eigensolver by Partitioning into Commuting Families" on Friday, January 17, 2020 at 1:30pm in CS 402.
by Nicki Mahler 10 Jan '20

10 Jan '20

Teague Tomesh will present his General Exam, "Minimizing State Preparations in Variational Quantum Eigensolver by Partitioning into Commuting Families" on Friday, January 17, 2020 at 1:30pm in CS 402. The members of his committee are as follows: Margaret Martonosi (adviser), Steve Lyon (EE), and Fred Chong (University of Chicago - Computer Science). 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. Variational quantum eigensolver (VQE) is a promising algorithm suitable for near-term quantum computers. VQE aims to approximate solutions to exponentially-sized optimization problems by executing a polynomial number of quantum subproblems. However, the number of subproblems scales as N^4 for typical problems of interest — a daunting growth rate that poses a serious limitation for emerging applications such as quantum computational chemistry. We mitigate this issue by exploiting the simultaneous measurability of subproblems corresponding to commuting terms. Our technique transpiles VQE instances into a format optimized for simultaneous measurement, yielding a linear-factor asymptotic improvement that translates to 8-30x lower cost for near term benchmarks. Our work also encompasses a synthesis tool for compiling simultaneous measurement circuits with minimal overhead. We demonstrate experimental validation of our techniques by estimating the ground state energy of deuteron with an IBM quantum computer. We also investigate the underlying statistics of simultaneous measurement and devise an adaptive strategy for mitigating harmful covariance terms. Textbook: Michael A Nielsen and Isaac L Chuang. Quantum computation and quantum information (10th anniv. version), 2010. Papers: 1. Richard Feynman. Simulating physics with computers. International Journal of Theoretical Physics, Vol 21, Now. 6/7, 1982 2. DiVincenzo, David P. "The physical implementation of quantum computation." Fortschritte der Physik: Progress of Physics/ 48, no. 9‐11 (2000): 771-783. 3. Peruzzo, Alberto, Jarrod McClean, Peter Shadbolt, Man-Hong Yung, Xiao-Qi Zhou, Peter J. Love, Alán Aspuru-Guzik, and Jeremy L. O’brien. "A variational eigenvalue solver on a photonic quantum processor." Nature communications 5 (2014): 4213. 4. Prakash Murali, Norbert Matthias Linke, Margaret Martonosi, Ali Javadi Abhari, Nhung Hong Nguyen, and Cinthia Huerta Alderete. 2019. Full-stack, real-system quantum computer studies: architectural comparisons and design insights. In Proceedings of the 46th International Symposium on Computer Architecture (ISCA '19). ACM, New York, NY, USA, 527-540. DOI: https://doi.org/10.1145/3307650.3322273 5. Preskill, John. "Quantum Computing in the NISQ era and beyond." Quantum 2 (2018): 79. 6. Tranter, Andrew, Peter J. Love, Florian Mintert, and Peter V. Coveney. "A Comparison of the Bravyi–Kitaev and Jordan–Wigner Transformations for the Quantum Simulation of Quantum Chemistry." Journal of chemical theory and computation 14, no. 11 (2018): 5617-5630. 7. X. Fu, M. A. Rol, C. C. Bultink, J. van Someren, N. Khammassi, I. Ashraf, R. F. L. Vermeulen, J. C. de Sterke, W. J. Vlothuizen, R. N. Schouten, C. G. Almudever, L. DiCarlo, and K. Bertels. 2017. An experimental microarchitecture for a superconducting quantum processor. In Proceedings of the 50th Annual IEEE/ACM International Symposium on Microarchitecture (MICRO-50 '17). ACM, New York, NY, USA, 813-825. DOI: https://doi.org/10.1145/3123939.3123952 8. Ravi Boppana and Magnús M Halldórsson. Approximating maximum independent sets by excluding subgraphs. BIT Numerical Mathematics, 32(2):180–196, 1992. 9. Jarrod R McClean,Jonathan Romero, Ryan Babbush, and Alán Aspuru-Guzik. The theory of variational hybrid quantum-classical algorithms. New Journal of Physics, 18(2):023023, 2016.

1 0

Alejandro Newell will present his General Exam "Beyond Objects: Image Understanding as Pixels to Graphs" on Friday, January 17, 2020 at 12pm in CS 401
by Nicki Mahler 10 Jan '20

10 Jan '20

Alejandro Newell will present his General Exam "Beyond Objects: Image Understanding as Pixels to Graphs" on Friday, January 17, 2020 at 12pm in CS 401. The members of his committee are as follows: Jia Deng (adviser), Olga Russakovsky, and Szymon Rusinkiewicz. 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: Tremendous progress has been made teaching computer vision systems to recognize objects in images. Each year, these systems can more reliably classify objects and better pinpoint their location in a scene. But a collection of objects is not enough. For full scene understanding, we must understand the connections and relationships between objects. Graphs are an effective way of representing these connections, but are difficult to express given standard approaches for training deep convolutional networks. In this presentation, I will discuss how to supervise a network to predict graphs. I will go over the details of our approach including its application to relationship detection and advantages over existing methods. Reading List: Szeliski, Richard. Computer vision: algorithms and applications. Springer Science & Business Media, 2010. Krizhevsky, Alex, Ilya Sutskever, and Geoffrey E. Hinton. "Imagenet classification with deep convolutional neural networks." Advances in neural information processing systems. 2012. Toshev, Alexander, and Christian Szegedy. "Deeppose: Human pose estimation via deep neural networks." Proceedings of the IEEE conference on computer vision and pattern recognition. 2014. Tompson, Jonathan J., et al. "Joint training of a convolutional network and a graphical model for human pose estimation." Advances in neural information processing systems. 2014. Johnson, Justin, et al. "Image retrieval using scene graphs." Proceedings of the IEEE conference on computer vision and pattern recognition. 2015. He, Kaiming, et al. "Deep residual learning for image recognition." Proceedings of the IEEE conference on computer vision and pattern recognition. 2016. Cao, Zhe, et al. "Realtime multi-person 2d pose estimation using part affinity fields." Proceedings of the IEEE Conference on Computer Vision and Pattern Recognition. 2017. He, Kaiming, et al. "Mask r-cnn." Proceedings of the IEEE international conference on computer vision. 2017. Krishna, Ranjay, et al. "Visual genome: Connecting language and vision using crowdsourced dense image annotations." International Journal of Computer Vision 123.1 (2017): 32-73. Lu, Cewu, et al. "Visual relationship detection with language priors." European Conference on Computer Vision. Springer, Cham, 2016. Xu, Danfei, et al. "Scene graph generation by iterative message passing." Proceedings of the IEEE Conference on Computer Vision and Pattern Recognition. 2017. Oord, Aaron van den, Yazhe Li, and Oriol Vinyals. "Representation learning with contrastive predictive coding." arXiv preprint arXiv:1807.03748 (2018).

1 0

Ziyang Xu will present his General Exam "Revisiting Type-Awareness for Automatic Parallelization" on Friday, January 17, 2020 at 10:30am in CS 302
by Nicki Mahler 10 Jan '20

10 Jan '20

Ziyang Xu will present his General Exam "Revisiting Type-Awareness for Automatic Parallelization" on Friday, January 17, 2020 at 10:30am in CS 302. The members of his committee are as follows: David August (adviser), Amit Levy, and Zachary Kincaid. 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: Over the last decade, advances in memory analyses, speculative techniques, and parallelization paradigms have dramatically improved the power of automatic parallelization. To be applicable for general-purpose C and C++ codes, parallelizing compilers incorporating these advances work without making use of type information. This study explores the value of making RAPPORT, a state-of-the-art parallelization framework, aware of modern type features when parallelizing Rust programs. We extend RAPPORT with a Rust frontend that brings type information to the IR. New type-aware memory analysis (TAMA) modules bring this information into the RAPPORT's collaborative analysis framework (CAF), allowing these modules to use type information in collaborating with other memory analysis modules to maximize their effect. We measure the extent to which this framework can use Rust type information to uncover more or better automatic parallelization opportunities. Reading List: Books: [1]J. L. Hennessy and D. A. Patterson, Computer architecture: a quantitative approach. Elsevier, 2011. [2]A. W. Appel, Modern Compiler Implementation in ML. New York, NY, USA: Cambridge University Press, 2004. Papers: [1]B. K. Rosen, M. N. Wegman, and F. K. Zadeck, “Global value numbers and redundant computations,” in Proceedings of the 15th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 1988, pp. 12–27. [2]D. G. Clarke, J. M. Potter, and J. Noble, “Ownership Types for Flexible Alias Protection,” in Proceedings of the 13th ACM SIGPLAN Conference on Object-oriented Programming, Systems, Languages, and Applications, New York, NY, USA, 1998, pp. 48–64. [3]A. Diwan, K. S. McKinley, and J. E. B. Moss, “Type-based Alias Analysis,” in Proceedings of the ACM SIGPLAN 1998 Conference on Programming Language Design and Implementation, New York, NY, USA, 1998, pp. 106–117. [4]K. Crary, D. Walker, and G. Morrisett, “Typed memory management in a calculus of capabilities,” in Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’99, San Antonio, Texas, United States, 1999, pp. 262–275. [5]G. Ottoni, R. Rangan, A. Stoler, and D. I. August, “Automatic thread extraction with decoupled software pipelining,” in 38th Annual IEEE/ACM International Symposium on Microarchitecture (MICRO’05), 2005, pp. 12 pp. – 118. [6]M. J. Bridges, N. Vachharajani, Y. Zhang, T. Jablin, and D. I. August, “Revisiting the Sequential Programming Model for Multi-Core,” in Proceedings of the 40th Annual IEEE/ACM International Symposium on Microarchitecture, pp. 69-84. IEEE Computer Society, 2007. [7]S. Campanoni, T. Jones, G. Holloway, V. J. Reddi, G.-Y. Wei, and D. Brooks, “HELIX: automatic parallelization of irregular programs for chip multiprocessing,” in Proceedings of the Tenth International Symposium on Code Generation and Optimization - CGO ’12, San Jose, California, 2012, p. 84. [8]N. P. Johnson, H. Kim, P. Prabhu, A. Zaks, and D. I. August, “Speculative Separation for Privatization and Reductions,” in Proceedings of the 33rd ACM SIGPLAN Conference on Programming Language Design and Implementation, New York, NY, USA, 2012, pp. 359–370. [9]N. P. Johnson, J. Fix, S. R. Beard, T. Oh, T. B. Jablin, and D. I. August, “A collaborative dependence analysis framework,” in 2017 IEEE/ACM International Symposium on Code Generation and Optimization (CGO), Austin, TX, USA, 2017, pp. 148–159. [10]V. Astrauskas, P. Müller, F. Poli, and A. J. Summers, “Leveraging Rust Types for Modular Specification and Verification,” Proc. ACM Program. Lang., vol. 3, no. OOPSLA, pp. 147:1–147:30, Oct. 2019. [11]S. Apostolakis, Z. Xu, G. Chan, S. Campanoni, and D. I. August, “Perspective: A Sensible Approach to Speculative Automatic Parallelization,” in Proceedings of the Twenty-Fifth International Conference on Architectural Support for Programming Languages and Operating Systems, 2020.

1 0

Aninda Manocha will present his General Exam, "Hardware-Software Co-Design to Accelerate Irregular Applications in the Post-Moore’s Law Era" on Wednesday, January 15, 2020 at 10am in CS 302
by Nicki Mahler 08 Jan '20

08 Jan '20

Aninda Manocha will present her General Exam, "Hardware-Software Co-Design to Accelerate Irregular Applications in the Post-Moore’s Law Era" on Wednesday, January 15, 2020 at 10am in CS 302. The members of her committee are as follows: Margaret Martonosi (adviser), David Wentzlaff, and David August 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. Despite their ubiquity in many important real-world, big-data applications, graph and other sparse applications remain difficult to accelerate even with modern accelerator-oriented, heterogeneous system designs. Many of these applications are characterized by irregular memory accesses caused by pointer indirection, which confounds caching mechanisms that hinge on the notion of locality as well as traditional prefetching and speculation techniques. As a result, these applications are bottlenecked by several long-latency memory accesses. First, my work approaches these workloads from a latency-tolerance perspective by proposing a Decoupled Access/Execute (DAE)-inspired technique, FAST-LLAMAs. This approach slices programs into Producer/Consumer threads and maps them onto simple in-order cores. Significant Memory-Level Parallelism (MLP) is then achieved in the form of dependency-free loads and asynchronous read-modify-write (RMWs) instructions issued on the Producer whose data is efficiently read by the Consumer. By using full-stack innovations in a simple, in-order, multi-core architecture, FAST-LLAMAs transforms long-latency memory accesses into requests that can issue asynchronously, thus hiding the cost of many costly accesses. With a single Producer/Consumer pair, FAST-LLAMAs yields a geomean of 4.21x and up to an 8.66x speedup over a single in-order core. Under the same area budget, the simple in-order cores of FAST-LLAMAs achieve a geomean of 11.79x and up to a 20.8x improvement in energy efficiency over out-of-order cores without requiring application-specific hardware. In order to address memory bandwidth limits of these irregular applications, my work then proposes reconfigurable, intelligent caching techniques called GSC (Graph-Specialized Caching) that optimize for separately allocated regions of memory employed in such applications. By isolating and specializing caching policies for the irregular memory accesses of such workloads, GSC techniques mimic a customized memory hierarchy with reconfigurability. More specifically, they employ logical cache partitioning, tailored access granularities, and node degree-based replacement policies to target irregular memory accesses. As a result, GSC techniques achieve a geomean of 1.70x and up to a 2.54x speedup, a geomean of 3.76x and up to 12.76x improvements in energy efficiency, and a geomean of 3.29x and up to a 4.74x improvement in bandwidth savings. This allows for parallel scaling far beyond what prior state-of-the-art memory hierarchies have achieved. Reading List James E. Smith. “Decoupled access/execute computer architectures.” In Proceedings of the 9th International Symposium on Computer Architecture (ISCA), pages 112-119. IEEE Press, 1982. James R. Goodman. “Using cache memory to reduce processor-memory traffic.” In Proceedings of the 10th International Symposium on Computer Architecture (ISCA), pages 124–131. ACM, 1983. Guilherme Ottoni, Ram Rangan, Adam Stoler, and David I. August, “Automatic thread extraction with decoupled software pipelining,” in Proceedings of the 38th International Symposium on Microarchitecture (MICRO), pages 107–118. IEEE Press, 2005. Mattan Erez, Jung Ho Ahn, Jayanth Gummaraju, Mendel Rosenblum, and William J. Dally. “Executing irregular scientific applications on stream architectures.” In Proceedings of the 21st International Conference on Supercomputing (ICS), pages 93–104. ACM, 2007. Carole-Jean Wu, Aamer Jaleel, Will Hasenplaugh, Margaret Martonosi, Simon C. Steely, Jr., and Joel Emer, “SHiP: Signature-based hit predictor for high performance caching.” In Proceedings of the 44th International Symposium on Microarchitecture (MICRO), pages 430–441. ACM, 2011. Tae Jun Ham, Juan L. Aragón, and Margaret Martonosi. “DeSC: Decoupled supply-compute communication management for heterogeneous architectures.” In Proceedings of the 48th International Symposium on Microarchitecture (MICRO), pages 191–203. ACM, 2015. Tae Jun Ham, Lisa Wu, Narayanan Sundaram, Nadathur Satish, and Margaret Martonosi. “Graphicionado: A high-performance and energy-efficient accelerator for graph analytics.” In Proceedings of the 49th International Symposium on Microarchitecture (MICRO), pages 1–13. IEEE Press, 2016. Sam Ainsworth and Timothy M. Jones. “An event-triggered programmable prefetcher for irregular workloads.” In Proceedings of the 23rd International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), pages 578–592. ACM, 2018. Abanti Basak, Shuangchen Li, Xing Hu, Sang Min Oh, Xinfeng Xie, Li Zhao, Xiaowei Jiang, and Yuan Xie. “Analysis and optimization of the memory hierarchy for graph processing workloads.” In Proceedings of the 2019 International Symposium on High Performance Computer Architecture (HPCA), pages 373–386. IEEE Press, 2019. Michael Pellauer, Yakun Sophia Shao, Jason Clemons, Neal Crago, Kartik Hegde, Rangharajan Venkatesan, Steven W. Keckler, Christopher W. Fletcher, and Joel Emer, “Buffets: An efficient and composable storage idiom for explicit decoupled data orchestration,” in Proceedings of the International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), pages 137-151. ACM, 2019. Textbook: John L. Hennessy and David A. Patterson. Computer Architecture: A Quantitative Approach. Morgan Kaufmann 5th edition (2011).

1 0

Zachary Teed will present his General Exam, "Video to Depth with Differentiable Structure from Motion" on Tuesday, January 14, 2020 at 4pm in CS 401
by Nicki Mahler 07 Jan '20

07 Jan '20

Zachary Teed will present his General Exam, "Video to Depth with Differentiable Structure from Motion" on Tuesday, January 14, 2020 at 4pm in CS 401. The members of his committee are Jia Deng (adviser), Olga Russakovsky, and Szymon Rusinkiewicz. 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. Title: Video to Depth with Differentiable Structure from Motion Abstract: In video to depth, the task is to estimate depth from a video sequence. This problem has traditionally been approached using Structure from Motion (SfM), which takes a collection of images as input, and jointly optimizes over 3D structure and camera motion. In parallel, deep learning has been highly successful on a number of 3D reconstruction tasks, but as recent work has shown, it is often hard to train generic network layers to directly utilize multiview geometry. We propose an end-to-end learning architecture for predicting depth from video which combines the representation ability of neural networks with the geometric principles governing image formation. We compose a collection of classical geometric algorithms, which are converted into trainable modules and combined into an end-to-end differentiable architecture. We evaluate our approach on 5 separate datasets, and outperform all existing single-view or multi-view approaches, while also demonstrating that our method can generalize across datasets. Textbook: Szeliski, Richard. Computer vision: algorithms and applications. Springer Science & Business Media, 2010. Papers: Engel, Jakob, Thomas Schöps, and Daniel Cremers. "LSD-SLAM: Large-scale direct monocular SLAM." European conference on computer vision. Springer, Cham, 2014. Engel, Jakob, Vladlen Koltun, and Daniel Cremers. "Direct sparse odometry." IEEE transactions on pattern analysis and machine intelligence 40.3 (2017): 611-625. Kümmerle, Rainer, et al. "g 2 o: A general framework for graph optimization." 2011 IEEE International Conference on Robotics and Automation. IEEE, 2011. Ranftl, Rene, et al. "Dense monocular depth estimation in complex dynamic scenes." Proceedings of the IEEE conference on computer vision and pattern recognition. 2016. Schonberger, Johannes L., and Jan-Michael Frahm. "Structure-from-motion revisited." Proceedings of the IEEE Conference on Computer Vision and Pattern Recognition. 2016. Quiroga, Julian, et al. "Dense semi-rigid scene flow estimation from rgbd images." European Conference on Computer Vision. Springer, Cham, 2014. Amos, Brandon, and J. Zico Kolter. "Optnet: Differentiable optimization as a layer in neural networks." Proceedings of the 34th International Conference on Machine Learning-Volume 70. JMLR. org, 2017. Dosovitskiy, Alexey, et al. "Flownet: Learning optical flow with convolutional networks." Proceedings of the IEEE international conference on computer vision. 2015. Kendall, Alex, et al. "End-to-end learning of geometry and context for deep stereo regression." Proceedings of the IEEE International Conference on Computer Vision. 2017. Tang, Chengzhou, and Ping Tan. "Ba-net: Dense bundle adjustment network." arXiv preprint arXiv:1806.04807 (2018). Zhou, Huizhong, Benjamin Ummenhofer, and Thomas Brox. "Deeptam: Deep tracking and mapping." Proceedings of the European Conference on Computer Vision (ECCV). 2018.

1 0

Zoe Paraskevopoulou will present her pre-FPO "An Verified Optimizing Backend for a Purely Functional Language" on January 14, 2020 in CS 402 at 10am
by Nicki Mahler 06 Jan '20

06 Jan '20

Zoe Paraskevopoulou will present her pre-FPO "An Verified Optimizing Backend for a Purely Functional Language" on January 14, 2020 in CS 402 at 10am. The members of her committee are: Andrew Appel (adviser), David Walker (reader), Amal Ahmed (Northeastern University), Aarti Gupta (non-reader), Zachary Kincaid (non-reader) Everyone is invited to attend her talk. The talk title and abstract follow below. An Verified Optimizing Backend for a Purely Functional Language --------------------------------------------------------------------------------------------------------- CertiCoq is a verified compiler for the source language of the interactive theorem prover Coq. The goal of CertiCoq is to bridge the gap between a certified source program and the compiled executable program. Coq's source language, Gallina, is a pure functional language without side effects. To allow programs to interact with their environment despite the lack of side effects, CertiCoq compiles Gallina to C, where the program can be linked with C code that handles the input and the output. In my thesis, I focus on the design, the implementation, and the verification of the optimizing backend of CertiCoq, that is responsible to efficiently compile untyped higher-order functional code to a first-order representation ready to be complied to C. The design of the CertiCoq backend follows a micropass compiler architecture that consists of small compiler passes each of them performing a simple task, and optimizations in the final code rely on the interaction of these transformations. To prove the set of backend transformations correct, I developed a proof framework based on step-indexed logical relations, a powerful proof technique that is used to show program equivalence. The modular and compositional nature of logical relations greatly fits the architecture of our compiler, allowing for proof reuse and compositional reasoning. Despite their mathematical elegance, logical relations cannot generally be used to show correctness of separate compilation in multi-pass compilers. I show how our existing proof framework can be extended to provide guarantees not only about whole-program compilation, but also about the correctness of the interaction of programs that are compiled separately through CertiCoq, perhaps using different backend optimizations. This is the first time that logical relations are used to obtain a proof of correctness for separate compilation. In the second part of my thesis, I show how to strengthen the guarantees that the proof framework provides, but from a different angle. Bugs in compilers manifest themselves not only in the final result of the computation, what we usually call functional correctness of the transformation, but also in other observable behaviours of the program, such as resource consumption. In order to ensure that a transformation will not introduce timing and memory leaks, I extended the logical relation framework so that it supports reasoning about preservation of running time and space. I used this extended proof framework to prove that the closure conversion algorithm of CertiCoq is not only correct with respect to the final result, but also safe for space. Furthermore, I also show that the garbage collection strategy followed by CertiCoq is safe with respect to the idealistic space consumption model. This is the first formal proof of space-safety for a closure conversion algorithm and a particular garbage collection strategy and also the first time that logical relations were used to reason about space safety.

1 0

Yixin Sun will present her FPO "Enhancing Anonymity Systems under Network and User Dynamics" on Tuesday, December 17, 2019 at 9:30am in CS 402.
by Nicki Mahler 09 Dec '19

09 Dec '19

Yixin Sun will present her FPO "Enhancing Anonymity Systems under Network and User Dynamics" on Tuesday, December 17, 2019 at 9:30am in CS 402. The members of her committee are as follows: Advisers: Mung Chiang and Prateek Mittal; Readers: Jennifer Rexford, Prateek Mittal, and Nick Feamster; Nonreaders: Jennifer Rexford, Ed Felten, and Mung Chiang. A copy of her thesis is available upon request. Please email ngotsis(a)cs.princeton if you would like a copy of the thesis. Everyone is invited to attend her talk. The talk title and abstract follow below. Privacy on the Internet is eroding rapidly. Anonymity systems have been designed to protect the identity and privacy of users from untrusted destinations and third parties on the Internet. However, many prior works on anonymity systems assume that important system components, such as network routing and user location, are static. In practice, these components are highly dynamic, leading to new vulnerabilities that can compromise user anonymity. In this dissertation, we exploit dynamics in anonymity systems across two different layers: network dynamics (i.e., changes in routing) at the network layer and user dynamics (i.e., changes in user location) at the application layer. First, we present RAPTOR attacks that exploit the dynamics in Internet routing to compromise user anonymity in the Tor network. The attacks enable adversaries to observe more user traffic and deanonymize them more effectively than previously thought. We successfully demonstrate the attacks by performing them on the live Tor network, ethically. Second, we build proactive and reactive defenses to protect Tor users from RAPTOR attacks: (1) a novel Tor relay selection algorithm that proactively reduces the probability of Tor users being affected by an attack, and (2) a monitoring system with novel detection analytics that detect routing anomaly for Tor relays in real time. Finally, we present attacks that exploit user mobility to compromise user anonymity across a wide range of anonymity systems. While prior works assume that user locations are fixed when accessing anonymity systems, we demonstrate that users can be highly mobile and subsequently expose themselves to adversaries as they visit more locations. In summary, we demonstrate the dangers of abstracting dynamics in Internet routing and user location from the analysis of anonymity systems, and take the step to design anonymity systems with these important system components in mind.

1 0

Colloquium Speaker Subhash Khot TODAY at 12:30pm
by Emily C. Lawrence 09 Dec '19

09 Dec '19

Distinguished CS Colloquium Speaker Subhash Khot, New York University Monday, December 9 - 12:30pm Computer Science - Room 105 Host: Ran Raz [ https://www.cs.princeton.edu/events/25898 | https://www.cs.princeton.edu/events/25898 ] Hardness of Approximation: From the PCP Theorem to the 2-to-2 Games Theorem Computer scientists firmly believe that no algorithm can efficiently compute optimal solutions to a class of problems called NP-hard problems. For many NP-hard problems, even computing an approximately optimal solution remains NP-hard. This phenomenon, known as the hardness of approximation, has numerous connections to proof checking, optimization, combinatorics , discrete Fourier analysis, and geometry. The talk will provide an overview of these connections. It will address why graph coloring is a computationally hard problem, how it is possible to check a proof without even looking at it, why computer scientists love the majority vote, and whether a shape exists that looks spherical as well as cubical. It will explain how all this fits into a 30-year research program starting with the foundational Probabilistically Checkable Proofs (PCP) Theorem and leading to the recent 2-to-2 Games Theorem. Bio: Subhash Khot is a professor of computer science at the Courant Institute of Mathematical Sciences at New York University. His prior affiliations include Princeton University (PhD), Institute for Advanced Study (member), Georgia Tech (assistant professor) and University of Chicago (visiting professor). His research centers on computational complexity and its connections to geometry and analysis. He is a recipient of the National Science Foundation’s Alan T. Waterman Award, the International Mathematical Union’s Nevanlinna Prize, the Simons Investigator Award, a MacArthur Fellowship, and is a Fellow of the Royal Society.

1 0

Reminder: Colloquium Speaker Subhash Khot, Monday Dec 9
by Emily C. Lawrence 06 Dec '19

06 Dec '19

Distinguished CS Colloquium Speaker Subhash Khot, New York University Monday, December 9 - 12:30pm Computer Science - Room 105 Host: Ran Raz [ https://www.cs.princeton.edu/events/25898 | https://www.cs.princeton.edu/events/25898 ] Hardness of Approximation: From the PCP Theorem to the 2-to-2 Games Theorem Computer scientists firmly believe that no algorithm can efficiently compute optimal solutions to a class of problems called NP-hard problems. For many NP-hard problems, even computing an approximately optimal solution remains NP-hard. This phenomenon, known as the hardness of approximation, has numerous connections to proof checking, optimization, combinatorics , discrete Fourier analysis, and geometry. The talk will provide an overview of these connections. It will address why graph coloring is a computationally hard problem, how it is possible to check a proof without even looking at it, why computer scientists love the majority vote, and whether a shape exists that looks spherical as well as cubical. It will explain how all this fits into a 30-year research program starting with the foundational Probabilistically Checkable Proofs (PCP) Theorem and leading to the recent 2-to-2 Games Theorem. Bio: Subhash Khot is a professor of computer science at the Courant Institute of Mathematical Sciences at New York University. His prior affiliations include Princeton University (PhD), Institute for Advanced Study (member), Georgia Tech (assistant professor) and University of Chicago (visiting professor). His research centers on computational complexity and its connections to geometry and analysis. He is a recipient of the National Science Foundation’s Alan T. Waterman Award, the International Mathematical Union’s Nevanlinna Prize, the Simons Investigator Award, a MacArthur Fellowship, and is a Fellow of the Royal Society.

1 0