Estimate the Memory Bounds Required by Shared Variables in Software Transactional Memory Programs

Estimating memory required by complex programs is a well-known research topic. In this work, we build a type system to statically estimate the memory bounds required by shared variables in software transactional memory (STM) programs. This work extends our previous works with additional language features such as explicitly declared shared variables, introduction of primitive types, and allowing loop body to contain any statement, not required to be well-typed as in our previous works. Also, the new type system has better compositionality compared to available type systems.

LooPy: interactive program synthesis with control structures

One vision for program synthesis, and specifically for programming by example (PBE), is an interactive programmer's assistant, integrated into the development environment. To make program synthesis practical for interactive use, prior work on Small-Step Live PBE has proposed to limit the scope of synthesis to small code snippets, and enable the users to provide local specifications for those snippets. This paradigm, however, does not work well in the presence of loops. We present LooPy, a synthesizer integrated into a live programming environment, which extends Small-Step Live PBE to work inside loops and scales it up to synthesize larger code snippets, while remaining fast enough for interactive use. To allow users to effectively provide examples at various loop iterations, even when the loop body is incomplete, LooPy makes use of live execution , a technique that leverages the programmer as an oracle to step over incomplete parts of the loop. To enable synthesis of loop bodies at interactive speeds, LooPy introduces Intermediate State Graph , a new data structure, which compactly represents a large space of code snippets composed of multiple assignment statements and conditionals. We evaluate LooPy empirically using benchmarks from competitive programming and previous synthesizers, and show that it can solve a wide variety of synthesis tasks at interactive speeds. We also perform a small qualitative user study which shows that LooPy's block-level specifications are easy for programmers to provide.

Point Orthogonal Projection onto a Spatial Algebraic Curve

Point orthogonal projection onto a spatial algebraic curve plays an important role in computer graphics, computer-aided geometric design, etc. We propose an algorithm for point orthogonal projection onto a spatial algebraic curve based on Newton’s steepest gradient descent method and geometric correction method. The purpose of Algorithm 1 in the first step of Algorithm 4 is to let the initial iteration point fall on the spatial algebraic curve completely and successfully. On the basis of ensuring that the iteration point fallen on the spatial algebraic curve, the purpose of the intermediate for loop body including Step 2 and Step 3 is to let the iteration point gradually approach the orthogonal projection point (the closest point) such that the distance between them is very small. Algorithm 3 in the fourth step plays an important double acceleration and orthogonalization role. Numerical example shows that our algorithm is very robust and efficient which it achieves the expected and ideal result.

Effects of the Aspect Ratio of a Rectangular Thermosyphon on Its Thermal Performance

The natural convection behaviors of rectangular thermosyphons with different aspect ratios were experimentally analyzed in this study. The experimental model consisted of a loop body, a heating section, a cooling section, and adiabatic sections. The heating and cooling sections were located in the vertical portions of the rectangular loop. The length of the vertical cooling section and the lengths of the upper and lower adiabatic sections were fixed at 300 mm and 200 mm, respectively. The inner diameter of the loop was fixed at 11 mm, and the cooling end temperature was 30 °C. The relevant parameters and their ranges were as follows: The aspect ratios were 6, 4.5, and 3.5 (with potential differences of 41, 27, and 18, respectively, between the cold and hot ends), and the input thermal power ranged from 30 to 60 W (with a heat flux of 600 to 3800 W/m2). The results show that it is feasible to obtain solar heat gain by installing a rectangular thermosyphon inside the metal curtain wall and that increasing the height of the opaque part of the metal curtain wall can increase the aspect ratio of the rectangular thermosyphon installed inside the wall and thus improve the heat transfer efficiency.

Floating-point Semantics of Analyzed Programs

This chapter focuses on floating-point semantics. It first outlines these semantics. The chapter then revisits previous results and adapts them to account for floating-point computations, assuming a bound on the rounding error is provided. A last part focuses on the approaches to bound these imprecisions, over-approximating the floating-point errors. Here, provided bounds on each variable, computing the floating-point error can be performed with classical interval-based analysis. Kleene-based iterations with interval abstract domain provide the appropriate framework to compute such bounds. This is even simpler in this setting because of the focus on bounding the floating-point error on a single call of the dynamic system transition function, that is, a single loop body execution without internal loops.

The Automation of C Program Verification by Symbolic Method of Loop Invariants Elimination

During deductive verification of programs written in imperative languages, the generation and proof of verification conditions corresponding to loops can cause difficulties, because each one must be provided with an invariant whose construction is often a challenge. As a rule, the methods of invariant synthesis are heuristic ones. This impedes its application. An alternative is the symbolic method of loop invariant elimination suggested by V.A. Nepomniaschy in 2005. Its idea is to represent a loop body in a form of special replacement operation under certain constraints. This operation expresses loop effect in a symbolic form and allows to introduce an inference rule which uses no invariants in axiomatic semantics. This work represents the further development of this method. It extends the mixed axiomatic semantics method suggested for C-light program verification. This extension includes the verification method of iterations over changeable arrays possibly with loop exit in C-light programs. The method contains the inference rule for iterations without loop invariants. This rule was implemented in verification conditions generator which is a part of the automated system of C-light program verification. To prove verification conditions automatically in ACL2, two algorithms were developed and implemented. The first one automatically generates the replacement operation in ACL2 language, the second one automatically generates auxiliary lemmas which allow to prove the obtained verification conditions in ACL2 successfully in automatic mode. An example which illustrates the application of the mentioned methods is described.