اشترك بالحزمة الذهبية واحصل على وصول غير محدود شمرا أكاديميا
تسجيل مستخدم جديدPeriodic Single-Pass Instruction Sequences
254
0
0.0
(
0
)
اسأل ChatGPT حول البحث
ﻻ يوجد ملخص باللغة العربية
A program is a finite piece of data that produces a (possibly infinite) sequence of primitive instructions. From scratch we develop a linear notation for sequential, imperative programs, using a familiar class of primitive instructions and so-called repeat instructions, a particular type of control instructions. The resulting mathematical structure is a semigroup. We relate this set of programs to program algebra (PGA) and show that a particular subsemigroup is a carrier for PGA by providing axioms for single-pass congruence, structural congruence, and thread extraction. This subsemigroup characterizes periodic single-pass instruction sequences and provides a direct basis for PGAs toolset.
قيم البحث
اقرأ أيضاً
Earlier work on program and thread algebra detailed the functional, observable behavior of programs under execution. In this article we add the modeling of unobservable, mechanistic processing, in particular processing due to jump instructions. We mo
del mechanistic processing preceding some further behavior as a delay of that behavior; we borrow a unary delay operator from discrete time process algebra. We define a mechanistic improvement ordering on threads and observe that some threads do not have an optimal implementation.
In program algebra, an algebraic theory of single-pass instruction sequences, three congruences on instruction sequences are paid attention to: instruction sequence congruence, structural congruence, and behavioural congruence. Sound and complete axi
om systems for the first two congruences were already given in early papers on program algebra. The current paper is the first one that is concerned with an axiom system for the third congruence. The presented axiom system is especially notable for its axioms that have to do with forward jump instructions.
We present a formal system for proving the partial correctness of a single-pass instruction sequence as considered in program algebra by decomposition into proofs of the partial correctness of segments of the single-pass instruction sequence concerne
d. The system is similar to Hoare logics, but takes into account that, by the presence of jump instructions, segments of single-pass instruction sequences may have multiple entry points and multiple exit points. It is intended to support a sound general understanding of the issues with Hoare-like logics for low-level programming languages.
For each function on bit strings, its restriction to bit strings of any given length can be computed by a finite instruction sequence that contains only instructions to set and get the content of Boolean registers, forward jump instructions, and a te
rmination instruction. We describe instruction sequences of this kind that compute the function on bit strings that models multiplication on natural numbers less than $2^N$ with respect to their binary representation by bit strings of length $N$, for a fixed but arbitrary $N > 0$, according to the long multiplication algorithm and the Karatsuba multiplication algorithm. We find among other things that the instruction sequence expressing the former algorithm is longer than the one expressing the latter algorithm only if the length of the bit strings involved is greater than $2^8$. We also go into the use of an instruction sequence with backward jump instructions for expressing the long multiplication algorithm. This leads to an instruction sequence that it is shorter than the other two if the length of the bit strings involved is greater than $2$.
In this paper, we study the phenomenon that instruction sequences are split into fragments which somehow produce a joint behaviour. In order to bring this phenomenon better into the picture, we formalize a simple mechanism by which several instructio
n sequence fragments can produce a joint behaviour. We also show that, even in the case of this simple mechanism, it is a non-trivial matter to explain by means of a translation into a single instruction sequence what takes place on execution of a collection of instruction sequence fragments.
سجل دخول لتتمكن من نشر تعليقات
التعليقات
جاري جلب التعليقات
سجل دخول لتتمكن من متابعة معايير البحث التي قمت باختيارها
