2015年的夏季学期在33名致远计算机科学方向大三学子的期盼中如约而至。作为致远学院与康奈尔大学计算机系共同举办的第二届暑期科研项目， 本次项目继续由康奈尔大学为学生开设了两门专业学分类的课程——“程序语言”和 “专业实践II”。 程序语言课程在教学中引入实践环节，所有致远学子在学习之余均可进入康奈尔大学计算机系的实验室进行实践学习。大部分同学在实验室里充分利用学习时间，几乎每天都学到很晚还不愿离开。
1:00pm, July 7: Lecture by Fred B. Schneider
1)Good theory takes practice;
3)Active vibration control system in airplanes uses a lot of gas in 1980s;
4)Reliable computers in airplanes needs to be designed;
5)SRI in Stanford.
1)Byzantine fault model: a model where anything goes;
2)t-Byzantine fault tolerant machine: a machine which can tolerate t Byzantine faults.
1)IC1: All non faulty agree on transmitter’s value;
2)IC2: If transmitter is non-faulty, then all non-faulty agree on the same value as the transmission had.
1:45pm, July 14: Lecture by Ken Birman
6)Fast & scalable.
1) Better tools for high assurance cloud computing;
2)Work with real users to demonstrate impact on nationally important, mission critical scenarios;
3)Push performance to the outer limits.
EXAMPLE: A “SMART” POWER GRID
1)Monitoring and dynamic control are vital to optimizing power delivery;
2)Renewables(solar, wind) are especially hard to manage, since they fluctuate a lot;
3)Recovery after major storm damage requires smart planning based on the state of the grid.
Machine Intelligence / A.I.
1) In fact these are exactly the same kinds of problems that researchers in ML/A.I. explore;
2) Grid cloud enable new forms of distributed collaboration tool.
Features of live distributed system varied.There are many challenges
ISIS2 IS AT THE CORE
1)Group communication system;
2)We use it in many ways and benefit from its strong security;
3)But speed has been a concern.
1)Core functionality: fault-toleration speed;
2)Intend for use in very hard large-scale setting;
3)The local object instance functions as a gate way;
4)Read-only operations performed on local state;
5)Update consistency; 6)Make the developer’s life easier; 7)Virtual consistency model.
Other ways to use ISIS2
1)CloudMake. HDRTFS. RDMA.
1:00pm, July 15: Lecture by Robbert van Renesse
The last decade or two have seen a wild growth of large-scale systems that have strongresponsiveness requirements. Such systems include cloud services as well as sensor networks.Their scalability and reliability requirements mandate that these systems are both sharded andreplicated. Also, these systems evolve quickly as a result of changes in workload, addingfunctionality, deploying new hardware, and so on. While these systems are useful, they canbehave in erratic ways and it is not clear that one can build mission- and life-critical systems this way.
Supercloud: Combining Cloud Resources into a Single Cloud
Infrastructure as a Service (IaaS) clouds couple applications tightly with the underlyinginfrastructures and services. This vendor lock-in problem forces users to apply ad-hoc deploymentstrategies in order to tolerate cloud failures, and limits the ability of doing virtual machine (VM) migration and resource scaling across different clouds, and even within availability zones of thesame cloud.
GridControl: Monitoring and Control of the Smart Power Grid
There are pressing economic and environmental arguments for the overhaul of the current power grid, and its replacement with a Smart Grid that integrates new kinds of green power generatingsystems, monitors power use, and adapts consumption to match power costs and system load.Many promising power management ideas demand scalability of a kind that seem a good ﬁt for cloud computing, but also have requirements (real-time, consistency, privacy, security, etc.) thatcloud computing does not currently support.
Conﬁguring Distributed Computations
Conﬁguring large distributed computations is a challenging task. Efﬁcient use of a cluster requires conﬁguration tuning and optimization based on careful examination of application and hardwareproperties. Considering the large number of parameters and impracticality of using trial and error ina production environment, cluster operators tend to make these decisions based on their experience and rules of thumb. Such conﬁgurations can lead to underutilized and costly clusters.
Reliable Broadcast for Geographically Dispersed Datacenters
Sprinkler is a reliable high-throughput broadcast facility for geographically dispersed datacenters.For scaling cloud services, datacenters use caching throughout their infrastructure. Sprinkler canbe used to broadcast update events that invalidate cache entries. The number of recipients canscale to many thousands in such scenarios. The Sprinkler infrastructure consists of two layers: onelayer to disseminate events among datacenters, and a second layer to disseminate events amongmachines within a datacenter. A novel garbage collection interface is introduced to save storagespace and network bandwidth.
Heterogeneous Failure Models
The robustness of distributed systems is usually phrased in terms of the number of failures ofcertain types that they can withstand. However, these failure models are too crude to describe thedifferent kinds of trust and expectations of participants in the modern world of complex, integratedsystems extending across different owners, networks, and administrative domains. Modernsystems often exist in an environment of heterogeneous trust, in which different participants may have different opinions about the trustworthiness of other nodes, and a single participant may consider other nodes to differ in their trustworthiness.
Correct-by-construction Fault-tolerant Distributed Systems
Fault-tolerant distributed systems, algorithms, and protocols are notoriously hard to build. Goingfrom a speciﬁcation to an implementation involves many subtle steps that are easy to get wrong.Moreover, fault-tolerant algorithms require many sources of diversity in order to make them survivea variety of failures. Programmers, even different ones, tend to make the same mistakes whenthey are implementing code from a speciﬁcation.
1:00pm, July 21: Lecture by Joseph Halpern
2:45pm, July 21: Lecture by Dexter Kozen
1)Introduce an informal view of coinduction and illustrate its use in math¬ematical arguments;
2)Argue that coindcution is not only about bisimilarity and equality of be¬haviors, butalso applicable toavarietyoffunctions andrelationsdeﬁnedon coinductive datatypes;
3)Aim to promote the principle as a useful tool for the working mathemati-cian and to bring it to a level of familarity on par with induction.
2)Induction vs Coinduction;
3)Lexicographic Order on Streams;
4)Transitivity of< lex;
5)Where is the Basis?
6)Monotonicity of + on Streams;
7)Coalgebras and Coalgebra Homomorphisms;
10)Bisimulations and Bisimilarity;
12)A Coinductive Proof Principle;