Exogenous-Loss Awareness in Queue Management: Toward Global Fairness

For a given TCP flow, exogenous losses are those occurring on links other than the flow's bottleneck link. Exogenous losses are typically viewed as introducing undesirable "noise" into TCP's feedback control loop, leading to inefficient network utilization and potentially severe global unfairness. This has prompted much research on mechanisms for hiding such losses from end-points. In this paper, we show through analysis and simulations that low levels of exogenous losses are surprisingly beneficial in that they improve stability and convergence, without sacrificing efficiency. Based on this, we argue that exogenous loss awareness should be taken into account in any AQM design that aims to achieve global fairness. To that end, we propose an exogenous-loss aware Queue Management (XQM) that actively accounts for and leverages exogenous losses. We use an equation based approach to derive the quiescent loss rate for a connection based on the connection's profile and its global fair share. In contrast to other queue management techniques, XQM ensures that a connection sees its quiescent loss rate, not only by complementing already existing exogenous losses, but also by actively hiding exogenous losses, if necessary, to achieve global fairness. We establish the advantages of exogenous-loss awareness using extensive simulations in which, we contrast the performance of XQM to that of a host of traditional exogenous-loss unaware AQM techniques.

The Ministry of Evil" An Examination of the Popular Bitter-Sweet Theology

Sermon by William Fairfield Warren.

Ubuntu, Jesus, and Earth: Integrating African Religion and Christianity in Ecological Ethics

Africa faces problems of ecological devastation caused by economic exploitation, rapid population growth, and poverty. Capitalism, residual colonialism, and corruption undermine Africa's efforts to forge a better future. The dissertation describes how in Africa the mounting ecological crisis has religious, political, and economic roots that enable and promote social and environmental harm. It presents the thesis that religious traditions, including their ethical expressions, can effectively address the crisis, ameliorate its impacts, and advocate for social and environmental betterment, now and in the future. First, it examines African traditional religion and Christian teaching, which together provide the foundation for African Christianity. Critical examination of both religious worldviews uncovers their complementary emphases on human responsibility toward planet Earth and future generations. Second, an analysis of the Gwembe Tonga of Chief Simamba explores the interconnectedness of all elements of the universe in African cosmologies. In Africa, an interdependent, participatory relationship exists between the world of animals, the world of humans, and the Creator. In discussing the annual lwiindi (rain calling) ceremony of Simamba, the study explores ecological overtones of African religions. Such rituals illustrate the involvement of ancestors and high gods in maintaining ecological integrity. Third, the foundation of the African morality of abundant life is explored. Across Sub-Saharan Africa, ancestors' teachings are the foundation of morality; ancestors are guardians of the land. A complementary teaching that Christ is the ecological ancestor of all life can direct ethical responses to the ecological crisis. Fourth, the eco-social implications of ubuntu (what it means to be fully human) are examined. Some aspects of ubuntu are criticized in light of economic inequalities and corruption in Africa. However, ubuntu can be transformed to advocate for eco-social liberation. Fifth, the study recognizes that in some cases conflicts exist between ecological values and religious teachings. This conflict is examined in terms of the contrast between awareness of socioeconomic problems caused by population growth, on the one hand, and advocacy of a traditional African morality of abundant children, on the other hand. A change in the latter religious view is needed since overpopulation threatens sustainable living and the future of Earth. The dissertation concludes that the identification of Jesus with African ancestors and theological recognition of Jesus as the ecological ancestor, woven together with ubuntu, an ethic of interconnectedness, should characterize African consciousness and promote resolution of the socio-ecological crisis.

Lightweight Formal Verification in Classroom Instruction of Reasoning about Functional Code

In college courses dealing with material that requires mathematical rigor, the adoption of a machine-readable representation for formal arguments can be advantageous. Students can focus on a specific collection of constructs that are represented consistently. Examples and counterexamples can be evaluated. Assignments can be assembled and checked with the help of an automated formal reasoning system. However, usability and accessibility do not have a high priority and are not addressed sufficiently well in the design of many existing machine-readable representations and corresponding formal reasoning systems. In earlier work [Lap09], we attempt to address this broad problem by proposing several specific design criteria organized around the notion of a natural context: the sphere of awareness a working human user maintains of the relevant constructs, arguments, experiences, and background materials necessary to accomplish the task at hand. We report on our attempt to evaluate our proposed design criteria by deploying within the classroom a lightweight formal verification system designed according to these criteria. The lightweight formal verification system was used within the instruction of a common application of formal reasoning: proving by induction formal propositions about functional code. We present all of the formal reasoning examples and assignments considered during this deployment, most of which are drawn directly from an introductory text on functional programming. We demonstrate how the design of the system improves the effectiveness and understandability of the examples, and how it aids in the instruction of basic formal reasoning techniques. We make brief remarks about the practical and administrative implications of the system’s design from the perspectives of the student, the instructor, and the grader.

Efficient Support for Common Relations in Lightweight Formal Reasoning Systems

In work that involves mathematical rigor, there are numerous benefits to adopting a representation of models and arguments that can be supplied to a formal reasoning or verification system: reusability, automatic evaluation of examples, and verification of consistency and correctness. However, accessibility has not been a priority in the design of formal verification tools that can provide these benefits. In earlier work [Lap09a], we attempt to address this broad problem by proposing several specific design criteria organized around the notion of a natural context: the sphere of awareness a working human user maintains of the relevant constructs, arguments, experiences, and background materials necessary to accomplish the task at hand. This work expands one aspect of the earlier work by considering more extensively an essential capability for any formal reasoning system whose design is oriented around simulating the natural context: native support for a collection of mathematical relations that deal with common constructs in arithmetic and set theory. We provide a formal definition for a context of relations that can be used to both validate and assist formal reasoning activities. We provide a proof that any algorithm that implements this formal structure faithfully will necessary converge. Finally, we consider the efficiency of an implementation of this formal structure that leverages modular implementations of well-known data structures: balanced search trees and transitive closures of hypergraphs.