Information for

2017 technical reports


Revisiting the CLBlood Model: Formulation Enhancements and Online Deployment


Spencer R. Van Leeuwen, Gladimir V. G. Baranoski and Bradley W. Kimmel


CLBlood is a cell-based light interaction model for human blood previously developed by the Natural Phenomena Simulation Group (NPSG) at the University of Waterloo. In this report, we revisit several elements of its formulation and describe appropriate enhancements. Furthermore, we compare our current and previous results to demonstrate that the predictive capabilities of our model have been fully preserved in its revised version. We also showcase the online deployment of CLBlood.

Date January 27, 2017
Report CS-2017-01 (PDF)

Renormalization of NoSQL Database Schemas


Michael J. Mior, Kenneth Salem


Applications using a NoSQL database may duplicate attribute values in multiple physical structures in order to provide additional access paths. This is necessary in order to meet performance goals but introduces complications. Typically, the NoSQL DBMS has no understanding of application-level denormalization. This means that if a user wishes to issue ad-hoc queries, it is necessary to understand this denormalization and to manually select which physical structures to use for a given query. Furthermore, if application requirements change, this often forces a change in the schema. This can impact existing application code which is no longer valid under the previous physical design.

We propose an algorithm for reconstructing a normalized logical schema from a denormalized physical design. Our method begins with a description of a denormalized physical schema along with functional and inclusion dependencies on this schema. By combining inference based on these dependencies with traditional normalization techniques, we produce a schema normalized according these dependencies which applications can be use as a logical model. This logical schema facilitates transparent optimization of ad-hoc queries using existing physical structures. We enable this optimization by also producing a mapping between the physical and logical schema as part of our normalization process. Furthermore, this logical schema is also useful as input to physical design tools in order to optimize the physical schema.

Date April 3, 2017
Report CS-2017-02 (PDF)

Database Managed CPU Performance Scaling for Improved Energy Efficiency


Mustafa Korkmaz, Martin Karsten, Kenneth Salem, Semih Salihoglu


Dynamic voltage and frequency scaling (DVFS) is a technique for adjusting the speed and power consumption of processors, allowing performance to be traded for reduced power consumption. Since CPUs are typically the largest consumers of power in modern  servers, DVFS can have a significant impact on overall server power consumption. Modern operating systems include DVFS governors, which interact with the processor to manage performance and power consumption according to some system-level policy.

In this paper, we argue that for database servers, DVFS can be managed more effectively by the database management system. We present a power-aware database request scheduling algorithm called POLARIS. Unlike operating system governors, POLARIS is aware of database units of work and database performance targets, and can achieve a better power/performance tradeoff by exploiting this knowledge. We implemented POLARIS in SHORE-MT, and we show that it can improve both power consumption and performance relative to operating system baselines.

Date June 2017
Report CS-2017-03 (PDF)

Symmetry Reduction and CompositionalVerification of Timed Automata


Linh Nguyen, Richard Trefler


Timed automata provide a model for studying thebehavior of finite-state systems as they evolve over time. We describe a technique that incorporates automatic symmetrydetection and symmetry reduction in the analysis of systemsmodeled by timed automata. Our prototype extends the realtimemodel checker PAT with symmetry reduction using stateswaps to reduce time and memory consumption. Moreover, ourapproach detects structural symmetries arising from processtemplates of real-time systems, requiring no additional inputfrom the user. The technique involves finding all variables of typeprocess identifier and computing the largest subgroup of candidatesymmetries that induce automorphisms. Our technique is fullyautomatic, and not restricted to fully symmetric systems. We thencombine elements of compositional proof, abstraction and localsymmetry to decide whether a safety property holds for everyprocess instance in a parameterized family of real-time processnetworks. Analysis is performed on a small cut-off network; thatis, a small instance whose compositional proof generalizes to theentire parametric family. Our results show that verification isdecidable in time polynomial in the state space of the cut-offinstance. We apply these ideas to analyze Fischer’s protocol andthe CSMA/CD protocol.

Date August 2017
Report CS-2017-04 (PDF)