Concise server-wide causality management for eventually consistent data stores

Large scale distributed data stores rely on optimistic replication to scale and remain highly available in the face of net work partitions. Managing data without coordination results in eventually consistent data stores that allow for concurrent data updates. These systems often use anti-entropy mechanisms (like Merkle Trees) to detect and repair divergent data versions across nodes. However, in practice hash-based data structures are too expensive for large amounts of data and create too many false conflicts. Another aspect of eventual consistency is detecting write conflicts. Logical clocks are often used to track data causality, necessary to detect causally concurrent writes on the same key. However, there is a nonnegligible metadata overhead per key, which also keeps growing with time, proportional with the node churn rate. Another challenge is deleting keys while respecting causality: while the values can be deleted, perkey metadata cannot be permanently removed without coordination. Weintroduceanewcausalitymanagementframeworkforeventuallyconsistentdatastores,thatleveragesnodelogicalclocks(BitmappedVersion Vectors) and a new key logical clock (Dotted Causal Container) to provides advantages on multiple fronts: 1) a new efficient and lightweight anti-entropy mechanism; 2) greatly reduced per-key causality metadata size; 3) accurate key deletes without permanent metadata.

Immersiveness of ubiquitous computing environments prototypes: A case study

The development of ubiquitous computing (ubicomp) environments raises several challenges in terms of their evaluation. Ubicomp virtual reality prototyping tools enable users to experience the system to be developed and are of great help to face those challenges, as they support developers in assessing the consequences of a design decision in the early phases of development. Given the situated nature of ubicomp environments, a particular issue to consider is the level of realism provided by the prototypes. This work presents a case study where two ubicomp prototypes, featuring different levels of immersion (desktop-based versus CAVE-based), were developed and compared. The goal was to determine the cost/benefits relation of both solutions, which provided better user experience results, and whether or not simpler solutions provide the same user experience results as more elaborate one.

Monitoring for a decidable fragment of MTL-∫

Temporal logics targeting real-time systems are traditionally undecidable. Based on a restricted fragment of MTL-R, we propose a new approach for the runtime verification of hard real-time systems. The novelty of our technique is that it is based on incremental evaluation, allowing us to e↵ectively treat duration properties (which play a crucial role in real-time systems). We describe the two levels of operation of our approach: offline simplification by quantifier removal techniques; and online evaluation of a three-valued interpretation for formulas of our fragment. Our experiments show the applicability of this mechanism as well as the validity of the provided complexity results.

Metaphorisms in programming

This paper introduces the metaphorism pattern of relational specification and addresses how specification following this pattern can be refined into recursive programs. Metaphorisms express input-output relationships which preserve relevant information while at the same time some intended optimization takes place. Text processing, sorting, representation changers, etc., are examples of metaphorisms. The kind of metaphorism refinement proposed in this paper is a strategy known as change of virtual data structure. It gives sufficient conditions for such implementations to be calculated using relation algebra and illustrates the strategy with the derivation of quicksort as example.

Using mouse dynamics to assess stress during online exams

"Lecture notes in computer science series", ISSN 0302-9743, vol. 9121

Definition of multibody system

This chapter presents a general view of multibody system concept and definition by describing the main features associated with spatial systems. The mechanical components, which can be modeled as rigid or flexible, are constrained by kinematic pair of different types. Additionally, the bodies can be actuated upon by force elements and external forces due to interaction with environment. This chapter also presents some examples of application of multibody systems that can include automotive vehicles, mechanisms, robots and biomechanical systems.

Fundamental concepts in multibody dynamics

In this chapter, the fundamental ingredients related to formulation of the equations of motion for multibody systems are described. In particular, aspects such as degrees of freedom, types of coordinates, basic kinematics joints and types of analysis in multibody systems are briefly characterized. Illustrative examples of application are also presented to better clarify the fundamental issues for spatial rigid multibody systems, which are of crucial importance in the formulation development of mathematical models of mechanical systems, as well as its computational implementation.

Global and local coordinates

This chapter described the global and local coordinate systems utilized in the formulation of spatial multibody systems. Global coordinate system is considered in the present work to denote the inertia frame. Additionally, body-fixed coordinate systems, also called local coordinate systems, are utilized to describe local properties of points that belong to a particular body. Furthermore, the process of transforming local coordinates into global coordinates is characterized by considering a transformation matrix. In the present work, Cartesian coordinates are utilized to locate the center of mass of each rigid body, as well as the location of any point that belongs to a body.

Euler angles, Bryant angles and Euler parameters

This chapter deals with the different approaches for describing the rotational coordinates in spatial multibody systems. In this process, Euler angles and Bryant angles are briefly characterized. Particular emphasis is given to Euler parameters, which are utilized to describe the rotational coordinates in the present work. In addition, for all the types of coordinates considered in this chapter, a characterization of the transformation matrix is fully described.

Angular velocity and acceleration

In this chapter, a complete characterization of the angular velocity and angular acceleration for rigid bodies in spatial multibody systems are presented. For both cases, local and global formulations are described taking into account the advantages of using Euler parameters. In this process, the transformation between global and local components of the angular velocity and time derivative of the Euler parameters are analyzed and discussed in this chapter.

Vector of coordinates, velocities and accelerations

This chapter describes the how the vector of coordinates are defined in the formulation of spatial multibody systems. For this purpose, the translational motion is described in terms of Cartesian coordinates, while rotational motion is specified using the technique of Euler parameters. This approach avoids the computational difficulties associated with the singularities in the case of using Euler angles or Bryant angles. Moreover, the formulation of the velocities vector and accelerations vector is presented and analyzed here. These two sets of vectors are defined in terms of translational and rotational coordinates.

Kinematic constraint equations

This chapter presents a general methodology for the formulation of the kinematic constraint equations at position, velocity and acceleration levels. Also a brief characterization of the different type of constraints is offered, namely the holonomic and nonholonomic constraints. The kinematic constraints described here are formulated using generalized coordinates. The chapter ends with a general approach to deal with the kinematic analysis of multibody systems.

Basic constraints between two vectors

This chapter deals with the characterization of the basic constraints between two vectors. This issue plays a crucial role in the formulation of constraint equations for mechanical joints. In particular, relations between two parallel and two perpendicular vectors are derived. Moreover, formulation for a vector that connects two generic points is presented. The material described here is developed under the framework of multibody systems formulation for spatial systems.

Kinematic joints constraints

"Series title: Springerbriefs in applied sciences and technology, ISSN 2191-530X"

Equations of motion for constrained systems

"Series title: Springerbriefs in applied sciences and technology, ISSN 2191-530X"