text:
# source:Papers/jar-cerco-2017/introduction.tex

Last change on this file was 3644, checked in by mulligan, 3 years ago

intro finished?

File size: 30.9 KB
Line
1\newcommand{\All}[1]{\forall{#1}.\;}
2\newcommand{\lam}[1]{\lambda{#1}.\;}
3
4% Introduction
5%   Problem being solved, background, etc.
6%   Current state of the art (and problem with it)
7%   The CerCo approach' (tm)
8%   Brief Matita overview
9%   Map of paper
10
11\section{Introduction}
12\label{sect.introduction}
13
14Programs are specified using both functional and non-functional constraints.
15Functional constraints dictate what tasks a program must do; non-functional constraints limit the resources the program may consume whilst completing those tasks.
16
17Depending on the application domain, non-functional constraints are as important as functional constraints when specifying a program.
18Real-time systems, with hard limits on application response times, implementations of cryptographic primitives, which must be hardened to timing side-channel attacks, and a heart pacemaker's embedded controller, which must fit inside a limited code memory space, are examples that fit this pattern.
19A cryptography library susceptible to a timing side-channel attack is not an annoyance---it's an implementation error that undermines the entire purpose of the library.
20
21A program's non-functional constraints may be given \emph{concretely}, or \emph{asymptotically}.
22Asymptotic complexity, as every Computer Science undergraduate knows, is important---but so too is concrete complexity for many applications, including the three we highlighted above as examples.
23Response times for a real time system are measured in seconds, milliseconds, or some other fundamental unit of time; a cryptographic library must have all execution paths execute in the same number of processor cycles, independent of any input passed by the client; the size of an embedded controller for a pacemaker is measured in bits, bytes, or some other unit of computer memory capacity.
24In all cases, resource consumption is measured (and is specified) in some basal, concrete unit of measure.
25
26Currently, a program's functional properties can be established by combining user annotations---preconditions, invariants, and so on---with various automated and semi-automated analyses---invariant generators, type systems, abstract interpretations, applications of theorem proving, and so on---on the high-level source code of the program.
27Functional properties of a program are therefore established by reasoning about the source code that the application programmer actually sees and writes.
28Further, the results of any analysis can be communicated to the programmer in terms of abstractions, control flow, and an overall system design that they are familiar with.
29
30By contrast, a program's concrete, non-functional properties are established by reasoning on low-level object code produced not by a programmer, but by a compiler.
31Whilst analyses operating at this level can and do produce very accurate results---Worst Case Execution Time (WCET) analysis can be extraordinarily accurate, for example---analysis at such a low-level of abstraction invariably has disadvantages:
32\begin{itemize}
33\item
34It can be hard to deduce the high-level structure of the program after compiler optimisations.
35The object code produced by an optimising compiler may have a radically different control flow to the original source code program.
36\item
37Object code analysis is unstable.
38Modern compilers and linkers are highly non-compositional: they implement a variety of sophisticated optimisation passes, and use an abundance of procedural, intra-procedural, module-level, and link-time analyses to direct these optimisations.
39As a result, small changes in high-level source code can produce radically different object code outputs from a compiler, affecting any analysis tied to that object code.
40\item
41It is well understood by Software Engineers that problems with the design or implementation of a program are cheaper to resolve early in the development process. %cite
42Despite this, techniques that operate on object code are not useful early in the development process of a program, where programs may be incomplete, with missing functionality, or missing modules.
43\item
44Parametric cost analysis is very hard: how can we translate a cost that depends on the execution state, for example the value of a register or a carry bit, to a cost that the user can understand whilst looking at the source code?
45\item
46Performing functional analysis on object code makes it hard for the programmer to provide information about the program and its expected execution, leading to a loss of precision in the resulting analysis.
47It is hard for the programmer to understand the results of the analysis, or direct its execution, as high-level abstractions, control flow constructs, and so on, introduced by the programmer are translated away'.
48\end{itemize}
49
50More ideal would be a high-level analysis of concrete, non-functional properties, coupled with the accuracy one would expect of e.g. existing WCET analysers.
51This would lead to a reconciliation of functional and non-functional analyses.
52Information could be shared between the two analyses, and both could be performed concurrently on the same high-level source code.
53
54What has previously prevented high-level reasoning about non-functional properties is the lack of a precise cost model for programs written in programming languages, such as C.
55As modern compilers---mentioned above---are inherently non-compositional in their translations, any precise concrete cost model for a high-level language must also be non-compositional, and is inherently tied to how an individual program is compiled.
56However, as optimisations may change control flow, and the cost of an object code instruction may depend on the runtime state of hardware components like pipelines and caches, none of which are visible in the source code, it has not been clear how one could go about defining such a cost model.
57
58In this paper, we report on the scientific and technical contributions of the Certified Complexity (CerCo') project~\cite{cerco}, an EU FET-Open funded collaboration between the Universities of Bologna, Edinburgh, and Paris 7.
59
60The central insight of the CerCo project is that a cost model for a high-level programming language can be defined using a compiler's implicit knowledge of how expressions and statements are translated to machine code.
61This implicit knowledge of how a compiler translates source-language phrases has to date been largely ignored when designing static analysis tools for concrete complexity measures.
62However, by embracing the compilation process itself, one is able to define a non-uniform, or non-compositional, cost model that is customised to the exact translation process that was subjected to the source-language program by the compiler.
63
64Accordingly, we first present a non-uniform, precise cost model for a large fragment of the C programming language---\emph{CerCo C}, which is based on early versions of \emph{CompCert C}~\cite{compcert}.
65To define this cost model, we have developed a technical device---dubbed \emph{the labelling approach}~\cite{labelling}---which is a technique to implement compilers that induce cost models on source programs by a very lightweight tracking of code changes through the compilation pipeline.
66
67To establish that this tracking works, and scales beyond toy' languages to more realistic programming languages, we have implemented a lightly-optimising compiler employing this technique.
68The \emph{CerCo verified C compiler} compiles the CerCo C language fragment to object binaries for the MCS-51 8-bit embedded microcontroller.
69This is a well-known and still popular processor in the embedded systems community.
70Our compiler lifts a cost-model induced on the machine code that it produces, back through the compilation chain, to the source-level, making use of the labelling approach to effect the tracking and lifting.
71At the source level, this cost model is made manifest as parametric cost-annotations, inserted into the original source code file of the program being compiled.
72These annotations may be used by the programmer to predict concrete execution time and stack space usage.
73
74As we are targeting an embedded microcontroller we have not considered dynamic memory allocation.
75However, we believe that our labelling approach is general enough to handle resources other than execution time and stack space usage, including dynamic memory allocation.
76
77To demonstrate source-level verification of costs we have implemented a Frama-C plugin~\cite{framac} that invokes our compiler on a source program and uses it to generate invariants on the high-level source that correctly model low-level costs.
78The plugin certifies that the program respects these costs by calling automated theorem provers, an innovative and novel technique in the field of static analysis for non-functional properties.
79Using this plugin, we have conducted case studies, including showing that the plugin can automatically compute and certify the exact reaction time of Lustre~\cite{lustre} data flow programs compiled into C.
80
81\subsection{Our approach in more detail}
82
83As mentioned above, in CerCo we reject the idea of a uniform, or compositional, cost model for a high-level programming language.
84We view any uniform cost model as being by its nature imprecise, as modern compilers themselves are highly non-compositional in their translations.
85Far better is to try to engineer the compiler---which knows how the code is translated---to return the cost model for basic blocks of high level instructions.
86To do this, the compiler must track modifications to the control flow of the program, in order to reverse them, and interface with a processor timing analysis.
87
88By embracing compilation, the CerCo compiler can both produce efficient code and return costs that are as precise as the processor timing analysis can be.
89Moreover, our costs can be parametric: the cost of a block can depend on actual program data, on a summary of the execution history, or on an approximated representation of the hardware state.
90
91For example, loop optimisations may assign a cost to a loop body that is a function of the number of iterations performed.
92As another example, the cost of a block may be a function of the vector of stalled pipeline states, which can be exposed in the source code and updated at each basic block exit.
93
94It is parametricity that allows one to analyse small code fragments without losing precision.
95In the analysis of the code fragment we do not have to ignore the initial hardware state; rather, we can assume that we know exactly which state (or mode, as the WCET literature calls it) we are in.
96Note that this approach also extends naturally to the early stages of program development.
97Users may axiomatically attach costs to unimplemented sub-components, or modules, which may be refined as program development proceeds.
98
99The CerCo approach is an improvement on the state of the art.
100By performing control and data flow analyses on the source code, the error-prone translation of invariants is avoided entirely.
101Instead, this work is done at the source code level using tools of the user's choice.
102Indeed, any available technique for the verification of functional properties can be easily reused and multiple techniques can collaborate to infer and certify cost invariants for the program.
103There are no limitations on the types of loops or data structures involved.
104Parametric cost analysis becomes the default, with non-parametric bounds used only as a last resort when the user decides to trade the complexity of the analysis for more precision.
105
106Note that we do not aim to supplant existing WCET analyses, but rather to augment and potentially embrace them as subcomponents of our own analysis.
107\emph{A priori}, no technique previously used in traditional WCET is obsolete: processor timing analysis can be used by the compiler on the object code, and other techniques can be applied at the source code level.
108In this work, we have instantiated the CerCo approach with a cost model for the MCS-51 hardware that our prototype compiler targets.
109As this hardware is relatively simple, it admits a precise cost model, and this is reflected in our final theorem, which demonstrates that our high-level cost annotations are both accurate and precise.
110On more modern hardware, exhibiting features such as caches, pipelines, and speculative execution, an exact cost model for time or space will be hard-to-impossible to define.
111Instead, existing WCET analyses could be used, and then lifted to high-level annotations using our non-standard compiler architecture.
112
113We take it as an article of faith that software used to verify other software must itself be as bug-free as possible---preferably verified itself.
114One way to achieve this is to reduce the trusted code base of any tools used.
115Here, trusted code base' refers to the corpus of code that must be trusted to believe that the analysis being carried out is accurate.
116The trusted code base of state-of-the-art static analysis tools, such as WCET analysers, is significant.
117These are sophisticated, complex pieces of software that are built around a control flow analyser, linear programming libraries, and also detailed formal models of the hardware under analysis.
118To trust a WCET tool, each of these subcomponents, along with their eventual combination, must all be trusted.
119
120In CerCo we move the control flow analysis to the source code level, and we introduce a non-standard compiler.
121As this compiler architecture is completely novel, we wish to ensure that our implementation (and by extension, our entire approach to lifting cost models) is correct.
122Therefore, to reduce the size of our trusted code base, we have implemented a prototype compiler and static analyser in an interactive theorem prover---Matita~\cite{matita,asperti:user:2007}, an implementation of the Calculus of Coinductive Constructions---which was used to certify that the cost annotations supplementing the program's source code are indeed an accurate reflection of those incurred by the hardware.
123We have also implemented formal models of the hardware and of the high-level source-language in the interactive theorem prover.
124
125Control flow analysis on the source code has been obtained using invariant generators, tools to produce proof obligations from generated invariants and automatic theorem provers to verify the obligations.
126If these tools are able to generate proof traces that can be independently checked, the only remaining component that enters the trusted code base is an off-the-shelf invariant generator which, in turn, can be proved correct using an interactive theorem prover.
127With these methods, we enable the use of more off-the-shelf components (e.g. provers and invariant generators) whilst reducing the trusted code base at the same time.
128
129\subsection{A proposed workflow}
130
131\begin{figure}[!t]
132\begin{tabular}{l@{\hspace{0.2cm}}|@{\hspace{0.2cm}}l}
133\begin{lstlisting}
134char a[] = {3, 2, 7, 14};
135char threshold = 4;
136
137int count(char *p, int len) {
138  char j;
139  int found = 0;
140  for (j=0; j < len; j++) {
141    if (*p <= threshold)
142      found++;
143    p++;
144    }
145  return found;
146}
147
148int main() {
149  return count(a,4);
150}
151\end{lstlisting}
152&
153%  $\vcenter{\includegraphics[width=7.5cm]{interaction_diagram.pdf}}$
154\begin{tikzpicture}[
155    baseline={([yshift=-.5ex]current bounding box)},
156    element/.style={draw, text width=1.6cm, on chain, text badly centered},
157    >=stealth
158    ]
159{[start chain=going below, node distance=.5cm]
160\node [element] (cerco) {CerCo\\compiler};
161\node [element] (cost)  {CerCo\\cost plugin};
162{[densely dashed]
163\node [element] (ded)   {Deductive\\platform};
164\node [element] (check) {Proof\\checker};
165}
166}
167\coordinate [left=3.5cm of cerco] (left);
168{[every node/.style={above, text width=3.5cm, text badly centered,
169                     font=\scriptsize}]
170\draw [<-] ([yshift=-1ex]cerco.north west) coordinate (t) --
171    node {C source}
172    (t-|left);
173\draw [->] (cerco) -- (cost);
174\draw [->] ([yshift=1ex]cerco.south west) coordinate (t) --
175    node {C source+\color{red}{cost annotations}}
176    (t-|left) coordinate (cerco out);
177\draw [->] ([yshift=1ex]cost.south west) coordinate (t) --
178    node {C source+\color{red}{cost annotations}\\+\color{blue}{synthesized assertions}}
179    (t-|left) coordinate (out);
180{[densely dashed]
181\draw [<-] ([yshift=-1ex]ded.north west) coordinate (t) --
182    node {C source+\color{red}{cost annotations}\\+\color{blue}{complexity assertions}}
183    (t-|left) coordinate (ded in) .. controls +(-.5, 0) and +(-.5, 0) .. (out);
184\draw [->] ([yshift=1ex]ded.south west) coordinate (t) --
185    node {complexity obligations}
186    (t-|left) coordinate (out);
187\draw [<-] ([yshift=-1ex]check.north west) coordinate (t) --
188    node {complexity proof}
189    (t-|left) .. controls +(-.5, 0) and +(-.5, 0) .. (out);
190\draw [dash phase=2.5pt] (cerco out) .. controls +(-1, 0) and +(-1, 0) ..
191    (ded in);
192}}
193%% user:
195\draw (current bounding box.west) ++(-.2,.5)
196    circle (.2) ++(0,-.2) -- ++(0,-.1) coordinate (t);
197% arms
198\draw (t) -- +(-.3,-.2);
199\draw (t) -- +(.3,-.2);
200% body
201\draw (t) -- ++(0,-.4) coordinate (t);
202% legs
203\draw (t) -- +(-.2,-.6);
204\draw (t) -- +(.2,-.6);
205\end{tikzpicture}
206\end{tabular}
207\caption{On the left: C code to count the number of elements in an array
208 that are less than or equal to a given threshold. On the right: CerCo's interaction
209 diagram. Components provided by CerCo are drawn with a solid border.}
210\label{test1}
211\end{figure}
212
213\fvset{commandchars=\\\{\}}
214\lstset{morecomment=[s][\color{blue}]{/*@}{*/},
215        moredelim=[is][\color{blue}]{$}{$},
216        moredelim=[is][\color{red}]{|}{|},
217        lineskip=-2pt}
218\begin{figure}[!p]
219\begin{lstlisting}
220|int __cost = 33, __stack = 5, __stack_max = 5;|
221|void __cost_incr(int incr) { __cost += incr; }|
222|void __stack_incr(int incr) {
223  __stack += incr;
224  __stack_max = __stack_max < __stack ? __stack : __stack_max;
225}|
226
227char a[4] = {3, 2, 7, 14};  char threshold = 4;
228
229/*@ behavior stack_cost:
230      ensures __stack_max <= __max(\old(__stack_max), 4+\old(__stack));
231      ensures __stack == \old(__stack);
232    behavior time_cost:
233      ensures __cost <= \old(__cost)+(178+214*__max(1+\at(len,Pre), 0));
234*/
235int count(char *p, int len) {
236  char j;  int found = 0;
237  |__stack_incr(4);  __cost_incr(111);|
238  $__l: /* internal */$
239  /*@ for time_cost: loop invariant
240        __cost <= \at(__cost,__l)+
241                  214*(__max(\at((len-j)+1,__l), 0)-__max(1+(len-j), 0));
242      for stack_cost: loop invariant
243        __stack_max == \at(__stack_max,__l);
244      for stack_cost: loop invariant
245        __stack == \at(__stack,__l);
246      loop variant len-j;
247  */
248  for (j = 0; j < len; j++) {
249    |__cost_incr(78);|
250    if (*p <= threshold) { |__cost_incr(136);| found ++; }
251    else { |__cost_incr(114);| }
252    p ++;
253  }
254  |__cost_incr(67);  __stack_incr(-4);|
255  return found;
256}
257
258/*@ behavior stack_cost:
259      ensures __stack_max <= __max(\old(__stack_max), 6+\old(__stack));
260      ensures __stack == \old(__stack);
261    behavior time_cost:
262      ensures __cost <= \old(__cost)+1358;
263*/
264int main(void) {
265  int t;
266  |__stack_incr(2);  __cost_incr(110);|
267  t = count(a,4);
268  |__stack_incr(-2);|
269  return t;
270}
271\end{lstlisting}
272\caption{The C program in Figure~\ref{test1} embellished with instrumentation added by the CerCo compiler in red and cost invariants added by the CerCo Frama-C plugin in blue.
273The \lstinline'__cost', \lstinline'__stack' and \lstinline'__stack_max' global variables hold the elapsed time in clock cycles and the current and maximum stack usage.
274Their initial values hold the clock cycles spent initialising global data in the preamble before calling \lstinline'main' and the space required by global data (and thus unavailable for the stack).
275}
276\label{itest1}
277\end{figure}
278
279How should a Software Engineer use the CerCo toolset in anger?
280We provide an illustrative C program on the left of Figure~\ref{test1}, along with a prospective workflow making use of our toolset on the right of Figure~\ref{test1}.
281An engineer writes their C program and feeds it as input to the CerCo compiler, which outputs an instrumented version of the same program that updates fresh global variables that record the elapsed execution time and the stack space usage.
282Figure~\ref{itest1} demonstrates one of the outputs of the CerCo C compiler---an embellished version of the original C source code, with cost annotations automatically inserted, the other output being an object code file, not included here.
283The red lines in Figure~\ref{itest1} introducing variables, functions and function calls starting with \lstinline'__cost' and \lstinline'__stack' are the instrumentation introduced by the compiler.
284For example, the two calls at the start of \lstinline'count' say that 4 bytes of stack are required, and that it takes 111 cycles to reach the next cost annotation (in the loop body).
285The compiler establishes these costs labelled object code that it generates, and lifts them back through the compilation chain, where they are finally reflected as cost annotations at the source level.
286
287The annotated program can then be enriched with complexity assertions in the style of Hoare logic, that are passed to a deductive platform (in our case Frama-C~\cite{framac}).
288We have written a simple automatic synthesiser for complexity assertions as a plugin for Frama-C.
289The behaviour of this plugin can be overridden by the user to increase or decrease accuracy.
290These are the blue comments starting with \lstinline'/*@' in Figure~\ref{itest1}, written in Frama-C's specification language, ACSL~\cite{acsl}.
291From these assertions, a general purpose deductive platform produces proof obligations which in turn can be closed by automatic or interactive provers, ending in a proof certificate.
292
293% NB: if you try this example with the live CD you should increase the timeout
294
295Twelve proof obligations are generated from Figure~\ref{itest1}.
296These obligations are to prove that the loop invariant holds after one execution if it holds before, to prove that the whole program execution takes at most 1358 cycles, and so on.
297Note that the synthesised time bound for \lstinline'count'---$178+214*(1+\text{\lstinline'len'})$ cycles---is parametric in the length of the array.
298The CVC3 SMT solver~\cite{DBLP:conf/cav/BarrettT07} closes all obligations within 30 seconds on commodity hardware.
299A simpler non-parametric version can be solved in seconds.
300
301\subsection{A brief introduction to Matita}
302
303We now briefly introduce Matita, the interactive theorem prover that was used in CerCo to certify all proofs.
304
305Matita is an interactive theorem proving system based on a variant of the Calculus of Coinductive Constructions~\cite{matita,asperti:user:2007}.
306The system features (co)inductive families of types, a system of coercions, a tactic-driven proof construction engine~\cite{sacerdoti-coen:tinycals:2007}, and paramodulation based automation~\cite{asperti:higher-order:2007}, all of which we exploit in the formalisation described herein.
307
308Matita's syntax is similar to the syntaxes of mainstream functional programming languages such as OCaml or Standard ML.
309The type theory that Matita implements is broadly akin to that of Coq~\cite{coq:2004} and Agda~\cite{bove:brief:2009}.
310Nevertheless, we provide a brief explanation of the main syntactic and type-theoretic features of Matita that will be needed to follow the body of the paper:
311\begin{itemize}
312\item
313Non-recursive functions and definitions are introduced via the \texttt{definition} keyword.
314Recursive functions are introduced with \texttt{let rec}.
315Mutually recursive functions are separated via the \texttt{and} keyword.
316Matita's termination checker ensures that all recursive functions are terminating before being admitted into the global environment, to maintain soundness.
317\item
318Matita has an infinite hierarchy of type universes.
319A single impredicative universe of types, \texttt{Prop}, exists at the base of this hierarchy.
320An unbounded series of predicative universes, \texttt{Type[0]}, \texttt{Type[1]}, \texttt{Type[2]}, and so on and so forth, sits atop \texttt{Prop}.
321One peculiarity of Matita is a user-customisable hierarchy of universes.
322In our development, we work in a context where \texttt{Prop} is contained in \texttt{Type[0]}, \texttt{Type[0]} is contained in \texttt{Type[1]}, and so on.
323Matita, unlike Coq or Agda, implements no form of typical ambiguity or universe polymorphism, with explicit concrete universe levels being preferred instead.
324\item
325Matita's type theory plays host to a rich and expressive higher-order logic.
326Constants \texttt{True} and \texttt{False} represent truth and falsity in \texttt{Prop} respectively.
327Two inductive families in \texttt{Prop} encode conjunction and disjunction---$\mathtt{P \wedge Q}$ and $\mathtt{P \vee Q}$ respectively.
328As is usual, implication and universal quantification are identified with the dependent function space ($\Pi$ types), whereas (constructive) existential quantification is encoded as a dependent sum (a $\Sigma$-type).
329We write $\All{x : \phi}\psi$ for the dependent function space, and abbreviate this as $\phi \rightarrow \psi$ when $x \not\in fv(\psi)$ as usual.
330We use $\langle M,N \rangle$ for the pairing of $M$ and $N$.
331\item
332Inductive and coinductive families are introduced via the \texttt{inductive} and \texttt{coinductive} keywords respectively, with named constructor declarations separated by a bar.
333Mutually inductive data family declarations are separated via \texttt{with}.
334In the following declaration:
335\begin{lstlisting}[language=Grafite]
336inductive I ($P_1$ : $\tau_1$) $\ldots$ ($P_n$ : $\tau_n$) : $\phi_1 \rightarrow \ldots \rightarrow \phi_m \rightarrow \phi$ := $\ldots$
337\end{lstlisting}
338We call $P_i$ for $0 \leq i \leq n$ the \textbf{parameters} of \texttt{I} and $\phi_j$ for $0 \leq j \leq m$ the \textbf{indices} of \texttt{I}.
339Matita's positivity checker ensures that constructors have strictly-positive types before admitting a (co)inductive family of types into the global environment, to maintain soundness.
340\item
341Records are introduced with the \texttt{record} keyword.
342A Matita record
343\begin{lstlisting}[language=Grafite]
344record R : Type[0] := { F1 : nat }.
345\end{lstlisting}
346may be thought of as syntactic sugar for a single-constructor inductive type of the same name:
347\begin{lstlisting}[language=Grafite]
348inductive R : Type[0] :=
349  | mk_R : nat -> R.
350\end{lstlisting}
351Types of later fields may depend on fields declared earlier in the record.
352Records may be decomposed with projections.
353Projections, one for each of field of a record, are registered in the global context.
354In the example record above, \texttt{F1} of type $R \rightarrow nat$ is registered as a field projection and $mk\_R$ of type $nat \rightarrow R$ is registered as a constructor.
355Record fields may also be marked as coercions.
356In the following example
357\begin{lstlisting}[language=Grafite]
358record S : Type[1] :=
359{
360  Carrier :> Type[0];
361  op : Carrier -> Carrier -> Carrier
362}
363\end{lstlisting}
364the field \texttt{Carrier} is declared to be a coercion with \texttt{:>}'.with the operational effect being that the field projection \texttt{Carrier} may be omitted where it could be successfully inferred by Matita.
365Field coercions facilitate the informal but common mathematical practice of intentionally confusing a structure with its underlying carrier set.
366\item
367Terms may be freely omitted, allowing the user to write down partial types and terms.
368A question mark, \texttt{?}, denotes a single term that has been omitted by the user.
369Some omitted terms can be deduced by Matita's refinement system~\cite{DBLP:journals/corr/abs-1202-4905}.
370Other, more complex goals arising from omitted terms may require user input to solve, in which case a proof obligation is opened for each term that cannot be deduced automatically.
371Three consecutive dots, \texttt{$\ldots$}, denote a vector of terms or types that have been omitted, and need to be inferred.
372\item
373(Co)data may be decomposed by pattern matching with a \texttt{match} expression.
374We may fully annotate a \texttt{match} expression with its return type.
375This is especially useful when working with indexed families of types or with invariants, expressed as types, on functions.
376In the following
377\begin{lstlisting}[language=Grafite]
378match t return $\lam{x}x = 0 \rightarrow bool$ with
379[ 0    $\Rightarrow$ $\lam{prf_1}P_1$
380| S m $\Rightarrow$ $\lam{prf_2}P_2$
381] (refl $\ldots$ t)
382\end{lstlisting}
383the \texttt{0} branch of the \texttt{match} expression returns a function from $0 = 0$ to \texttt{bool}, whereas the \texttt{S m} branch of the \texttt{match} expression returns a function from \texttt{S m = 0} to \texttt{bool}.
384In both cases the annotated return type $\lam{x}x = 0 \rightarrow bool$ has been specialised given new information about \texttt{t} revealed by the act of pattern matching.
385The entire term, with \texttt{match} expression applied to \texttt{refl $\ldots$ t}, has type \texttt{bool}.
386\item
387Matita features a liberal system of coercions (distinct from the previously mentioned record field coercions).
388It is possible to define a uniform coercion $\lam{x}\langle x, ?\rangle$ from every type $T$ to the dependent product $\Sigma{x : T}. P x$.
389The coercion opens a proof obligation that asks the user to prove that $P$ holds for $x$.
390When a coercion is to be applied to a complex term (for example, a $\lambda$-abstraction, a local definition, or a case analysis), the system automatically propagates the coercion to the sub-terms.
391For instance, to apply a coercion to force $\lam{x}M : A \rightarrow B$ to
392have type $\All{x : A}\Sigma{y : B}. P x y$, the system looks for a coercion from $M : B$ to $\Sigma{y : B}. P x y$ in a context augmented with $x : A$.
393This is significant when the coercion opens a proof obligation, as the user will be presented with multiple, but simpler proof obligations in the correct context.
394In this way, Matita supports the Russell' proof methodology developed by Sozeau in~\cite{sozeau:subset:2007}, in a lightweight but tightly-integrated manner.
395\end{itemize}
396Throughout, for reasons of clarity, conciseness, and readability, we may choose to simplify or omit parts of Matita code.
397We will always ensure that these omissions do not mislead the reader.
398
399\subsection{Map of the paper}
400
401The rest of the paper is structured as follows:
402
403In Section~\ref{sect.compiler.architecture}, we describe the architecture of the CerCo compiler.
404We describe the compiler's intermediate languages, from CerCo C down to MCS-51 machine code, and their formal semantics.
405We also describe the optimisations that the CerCo verified C compiler implements.
406
407In Section~\ref{sect.compiler.proof}, we describe the proof of correctness of the compiler in more detail.
408We explain \emph{structured traces}, a technical device developed to complete the proof, and our labelling approach.
409We further discuss the verification of our translation and optimisation passes for the intermediate languages, and discuss our verified assembler.
410
411In Section~\ref{sect.formal.development}, we present statistical data on the formal development, including line counts, and so on, and discuss remaining axioms in our proof of the compiler's correctness.
412We also briefly discuss lessons learnt' in the formal development of the CerCo verified C compiler.
413
414In Section~\ref{sect.framac.plugin}, we discuss the Frama-C plugin for certifying the concrete complexity of programs written in CerCo C.
415We also present a case study, demonstrating the plugin in action.
416
417Finally, in Section~\ref{sect.conclusions} we conclude, discussing related and future work.
Note: See TracBrowser for help on using the repository browser.


text:
시간 제한메모리 제한제출정답맞힌 사람정답 비율
1 초 256 MB137777.778%

문제

Once upon a time, Mr. Cool created a tree (an undirected graph without cycles) of n vertices, by assigning to each vertex i > 1 two numbers: pi < i — the direct ancestor of vertex i and wi — the weight of the edge between vertex i and pi. Vertex 1 is the root, so it does not have any ancestors.

You wanted to know what tree did Mr. Cool build, but Mr. Cool refused to tell this, but he gave you a tip:

He wrote all these numbers in one line. That’s how he got array b of length 2 · n − 2.

b = [p2, w2, p3, w3, . . . , pn−1, wn−1, pn, wn]

Then he randomly shuffled it. That’s how he got array a, and Mr. Cool presented you with it.

Since it is impossible to restore the tree knowing only values of array a, you decided to solve a different problem.

Let’s call a tree k-long, if there are exactly k edges on the path between vertex 1 and n.

Let’s call a tree k-perfect, if it is k-long and the sum of the weights of the edges on the path between vertex 1 and vertex n is maximal among all possible k-long trees that Mr. Cool could build.

Your task is to print the sum of the weights of the edges on the path between vertex 1 and vertex n for all possible k-perfect trees or print −1 if a certain k-long tree could not be built by Mr. Cool.

입력

The first line contains one integer n (2 ≤ n ≤ 105) — the number of the vertices in the tree.

The second line contains 2 · n − 2 integers a1, a2, . . . , a2n−2 (1 ≤ ai ≤ n − 1) — the elements of array a.

출력

In one line, print n − 1 space-separated integers w1, w2, w3, . . . , wn−1, where wk — the sum of the weights of the edges on the path between vertex 1 and vertex n in a k-perfect tree. If there is no i-long tree, then wi should be equal to −1.

예제 입력 1

3
1 1 2 2

예제 출력 1

2 3

예제 입력 2

3
2 2 2 2

예제 출력 2

-1 -1

예제 입력 3

6
1 4 5 4 4 4 3 4 4 2

예제 출력 3

-1 -1 -1 17 20

힌트

In the first example, the 1-perfect tree is defined by array [1, 2, 1, 2] (i.e. p2 = 1, w2 = 2, p3 = 1, w3 = 2). The 2-perfect tree is defined by array [1, 2, 2, 1] (i.e p2 = 1, w2 = 2, p3 = 2, w3 = 1). Here are illustrations of the 1-perfect tree and the 2-perfect tree respectively (path from vertex 1 to vertex n is drawn with bold lines):

In the second example, there are no k-perfect trees, that can be obtained by permuting array a.

In the third example, only 4-perfect tree and 5-perfect tree can be obtained. These are defined by arrays [1, 4, 2, 4, 3, 4, 4, 4, 4, 5] and [1, 4, 2, 4, 3, 4, 4, 4, 5, 4] respectively. Here are illustrations of them:

format: plain


text:
## 21.29 Comparing two topologies, II

Let $\mathcal{C}$ be a category. Let $\text{Cov}(\mathcal{C}) \supset \text{Cov}'(\mathcal{C})$ be two ways to endow $\mathcal{C}$ with the structure of a site. Denote $\tau$ the topology corresponding to $\text{Cov}(\mathcal{C})$ and $\tau '$ the topology corresponding to $\text{Cov}'(\mathcal{C})$. Then the identity functor on $\mathcal{C}$ defines a morphism of sites

$\epsilon : \mathcal{C}_\tau \longrightarrow \mathcal{C}_{\tau '}$

where $\epsilon _*$ is the identity functor on underlying presheaves and where $\epsilon ^{-1}$ is the $\tau$-sheafification of a $\tau '$-sheaf (hence clearly exact). Let $\mathcal{O}$ be a sheaf of rings for the $\tau$-topology. Then $\mathcal{O}$ is also a sheaf for the $\tau '$-topology and $\epsilon$ becomes a morphism of ringed sites

$\epsilon : (\mathcal{C}_\tau , \mathcal{O}_\tau ) \longrightarrow (\mathcal{C}_{\tau '}, \mathcal{O}_{\tau '})$

For more discussion, see Section 21.27.

Lemma 21.29.1. With $\epsilon : (\mathcal{C}_\tau , \mathcal{O}_\tau ) \to (\mathcal{C}_{\tau '}, \mathcal{O}_{\tau '})$ as above. Let $\mathcal{B} \subset \mathop{\mathrm{Ob}}\nolimits (\mathcal{C})$ be a subset. Let $\mathcal{A} \subset \textit{PMod}(\mathcal{O})$ be a full subcategory. Assume

1. every object of $\mathcal{A}$ is a sheaf for the $\tau$-topology,

2. $\mathcal{A}$ is a weak Serre subcategory of $\textit{Mod}(\mathcal{O}_\tau )$,

3. every object of $\mathcal{C}$ has a $\tau '$-covering whose members are elements of $\mathcal{B}$, and

4. for every $U \in \mathcal{B}$ we have $H^ p_\tau (U, \mathcal{F}) = 0$, $p > 0$ for all $\mathcal{F} \in \mathcal{A}$.

Then $\mathcal{A}$ is a weak Serre subcategory of $\textit{Mod}(\mathcal{O}_{\tau '})$ and there is an equivalence of triangulated categories $D_\mathcal {A}(\mathcal{O}_\tau ) = D_\mathcal {A}(\mathcal{O}_{\tau '})$ given by $\epsilon ^*$ and $R\epsilon _*$.

Proof. Since $\epsilon ^{-1}\mathcal{O}_{\tau '} = \mathcal{O}_\tau$ we see that $\epsilon$ is a flat morphism of ringed sites and that in fact $\epsilon ^{-1} = \epsilon ^*$ on sheaves of modules. By property (1) we can think of every object of $\mathcal{A}$ as a sheaf of $\mathcal{O}_\tau$-modules and as a sheaf of $\mathcal{O}_{\tau '}$-modules. In other words, we have fully faithful inclusion functors

$\mathcal{A} \to \textit{Mod}(\mathcal{O}_\tau ) \to \textit{Mod}(\mathcal{O}_{\tau '})$

To avoid confusion we will denote $\mathcal{A}' \subset \textit{Mod}(\mathcal{O}_{\tau '})$ the image of $\mathcal{A}$. Then it is clear that $\epsilon _* : \mathcal{A} \to \mathcal{A}'$ and $\epsilon ^* : \mathcal{A}' \to \mathcal{A}$ are quasi-inverse equivalences (see discussion preceding the lemma and use that objects of $\mathcal{A}'$ are sheaves in the $\tau$ topology).

Conditions (3) and (4) imply that $R^ p\epsilon _*\mathcal{F} = 0$ for $p > 0$ and $\mathcal{F} \in \mathop{\mathrm{Ob}}\nolimits (\mathcal{A})$. This is true because $R^ p\epsilon _*$ is the sheaf associated to the presheave $U \mapsto H^ p_\tau (U, \mathcal{F})$, see Lemma 21.8.4. Thus any exact complex in $\mathcal{A}$ (which is the same thing as an exact complex in $\textit{Mod}(\mathcal{O}_\tau )$ whose terms are in $\mathcal{A}$, see Homology, Lemma 12.9.3) remains exact upon applying the functor $\epsilon _*$.

Consider an exact sequence

$\mathcal{F}'_0 \to \mathcal{F}'_1 \to \mathcal{F}'_2 \to \mathcal{F}'_3 \to \mathcal{F}'_4$

in $\textit{Mod}(\mathcal{O}_{\tau '})$ with $\mathcal{F}'_0, \mathcal{F}'_1, \mathcal{F}'_3, \mathcal{F}'_4$ in $\mathcal{A}'$. Apply the exact functor $\epsilon ^*$ to get an exact sequence

$\epsilon ^*\mathcal{F}'_0 \to \epsilon ^*\mathcal{F}'_1 \to \epsilon ^*\mathcal{F}'_2 \to \epsilon ^*\mathcal{F}'_3 \to \epsilon ^*\mathcal{F}'_4$

in $\textit{Mod}(\mathcal{O}_\tau )$. Since $\mathcal{A}$ is a weak Serre subcategory and since $\epsilon ^*\mathcal{F}'_0, \epsilon ^*\mathcal{F}'_1, \epsilon ^*\mathcal{F}'_3, \epsilon ^*\mathcal{F}'_4$ are in $\mathcal{A}$, we conclude that $\epsilon ^*\mathcal{F}_2$ is in $\mathcal{A}$ by Homology, Definition 12.9.1. Consider the map of sequences

$\xymatrix{ \mathcal{F}'_0 \ar[r] \ar[d] & \mathcal{F}'_1 \ar[r] \ar[d] & \mathcal{F}'_2 \ar[r] \ar[d] & \mathcal{F}'_3 \ar[r] \ar[d] & \mathcal{F}'_4 \ar[d] \\ \epsilon _*\epsilon ^*\mathcal{F}'_0 \ar[r] & \epsilon _*\epsilon ^*\mathcal{F}'_1 \ar[r] & \epsilon _*\epsilon ^*\mathcal{F}'_2 \ar[r] & \epsilon _*\epsilon ^*\mathcal{F}'_3 \ar[r] & \epsilon _*\epsilon ^*\mathcal{F}'_4 }$

The lower row is exact by the discussion in the preceding paragraph. The vertical arrows with index $0$, $1$, $3$, $4$ are isomorphisms by the discussion in the first paragraph. By the $5$ lemma (Homology, Lemma 12.5.20) we find that $\mathcal{F}'_2 \cong \epsilon _*\epsilon ^*\mathcal{F}'_2$ and hence $\mathcal{F}'_2$ is in $\mathcal{A}'$. In this way we see that $\mathcal{A}'$ is a weak Serre subcategory of $\textit{Mod}(\mathcal{O}_{\tau '})$, see Homology, Definition 12.9.1.

At this point it makes sense to talk about the derived categories $D_\mathcal {A}(\mathcal{O}_\tau )$ and $D_{\mathcal{A}'}(\mathcal{O}_{\tau '})$, see Derived Categories, Section 13.13. To finish the proof we show that conditions (1) – (5) of Lemma 21.28.7 apply. We have already seen (1), (2), (3) above. Note that since every object has a $\tau '$-covering by objects of $\mathcal{B}$, a fortiori every object has a $\tau$-covering by objects of $\mathcal{B}$. Hence condition (4) of Lemma 21.28.7 is satisfied. Similarly, condition (5) is satisfied as well. $\square$

Lemma 21.29.2. With $\epsilon : (\mathcal{C}_\tau , \mathcal{O}_\tau ) \to (\mathcal{C}_{\tau '}, \mathcal{O}_{\tau '})$ as above. Let $A$ be a set and for $\alpha \in A$ let

$\xymatrix{ E_\alpha \ar[d] \ar[r] & Y_\alpha \ar[d] \\ Z_\alpha \ar[r] & X_\alpha }$

be a commutative diagram in the category $\mathcal{C}$. Assume that

1. a $\tau '$-sheaf $\mathcal{F}'$ is a $\tau$-sheaf if $\mathcal{F}'(X_\alpha ) = \mathcal{F}'(Z_\alpha ) \times _{\mathcal{F}'(E_\alpha )} \mathcal{F}'(Y_\alpha )$ for all $\alpha$,

2. for $K'$ in $D(\mathcal{O}_{\tau '})$ in the essential image of $R\epsilon _*$ the maps $c^{K'}_{X_\alpha , Z_\alpha , Y_\alpha , E_\alpha }$ of Lemma 21.26.1 are isomorphisms for all $\alpha$.

Then $K' \in D^+(\mathcal{O}_{\tau '})$ is in the essential image of $R\epsilon _*$ if and only if the maps $c^{K'}_{X_\alpha , Z_\alpha , Y_\alpha , E_\alpha }$ are isomorphisms for all $\alpha$.

Proof. The “only if” direction is implied by assumption (2). On the other hand, if $K'$ has a unique nonzero cohomology sheaf, then the “if” direction follows from assumption (1). In general we will use an induction argument to prove the “if” direction. Let us say an object $K'$ of $D^+(\mathcal{O}_{\tau '})$ satisfies (P) if the maps $c^{K'}_{X_\alpha , Z_\alpha , Y_\alpha , E_\alpha }$ are isomorphisms for all $\alpha \in A$.

Namely, let $K'$ be an object of $D^+(\mathcal{O}_{\tau '})$ satisfying (P). Choose a bounded below complex ${\mathcal{K}'}^\bullet$ of sheaves of $\mathcal{O}_{\tau '}$-modules representing $K'$. We will show by induction on $n$ that we may assume for $p \leq n$ we have $(\mathcal{K}')^ p = \epsilon _*\mathcal{J}^ p$ for some injective sheaf $\mathcal{J}^ p$ of $\mathcal{O}_{\tau }$-modules. The assertion is true for $n \ll 0$ because $(\mathcal{K}')^\bullet$ is bounded below.

Induction step. Assume we have $(\mathcal{K}')^ p = \epsilon _*\mathcal{J}^ p$ for some injective sheaves $\mathcal{J}^ p$ of $\mathcal{O}_\tau$-modules for $p \leq n$. Denote $\mathcal{J}^\bullet$ the bounded complex of injective $\mathcal{O}_\tau$-modules made from these sheaves and the maps between them. Consider the short exact sequence of complexes

$0 \to \sigma _{\geq n + 1}(\mathcal{K}')^\bullet \to (\mathcal{K}')^\bullet \to \epsilon _*\mathcal{J}^\bullet \to 0$

where $\sigma _{\geq n + 1}$ denotes the “stupid” truncation. By assumption (2) the object $\epsilon _*\mathcal{J}^\bullet$ of $D(\mathcal{O}_{\tau '})$ satisfies (P). By Lemma 21.26.2 we conclude that $\sigma _{\geq n + 1}(\mathcal{K}')^\bullet$ satisfies (P). We conclude that for $\alpha \in A$ the sequence

$\begin{matrix} 0 \\ \downarrow \\ H^{n + 1}_{\tau '}(X_\alpha , \sigma _{\geq n + 1}(\mathcal{K}')^\bullet ) \\ \downarrow \\ H^{n + 1}_{\tau '}(Z_\alpha , \sigma _{\geq n + 1}(\mathcal{K}')^\bullet ) \oplus H^{n + 1}_{\tau '}(Y_\alpha , \sigma _{\geq n + 1}(\mathcal{K}')^\bullet ) \\ \downarrow \\ H^{n + 1}_{\tau '}(E_\alpha , \sigma _{\geq n + 1}(\mathcal{K}')^\bullet ) \end{matrix}$

is exact by the distinguished triangle of Lemma 21.26.1 and the fact that $\sigma _{\geq n + 1}(\mathcal{K}')^\bullet$ has vanishing cohomology over $E_\alpha$ in degrees $< n + 1$. We conclude that

$\mathcal{F}' = \mathop{\mathrm{Ker}}((\mathcal{K}')^{n + 1} \to (\mathcal{K}')^{n + 2})$

is a $\tau$-sheaf by assumption (1) because the cohomology groups above evaluate to $\mathcal{F}'(X_\alpha )$, $\mathcal{F}'(Z_\alpha ) \oplus \mathcal{F}'(Y_\alpha )$, and $\mathcal{F}'(E_\alpha )$. Thus we may choose an injective $\mathcal{O}_\tau$-module $\mathcal{J}^{n + 1}$ and an injection $\mathcal{F}' \to \epsilon _*\mathcal{J}^{n + 1}$. Since $\epsilon _*\mathcal{J}^{n + 1}$ is also an injective $\mathcal{O}_{\tau '}$-module (Lemma 21.15.2) we can extend $\mathcal{F}' \to \epsilon _*\mathcal{J}^{n + 1}$ to a map $(\mathcal{K}')^{n + 1} \to \epsilon _*\mathcal{J}^{n + 1}$. Then the complex $(\mathcal{K}')^\bullet$ is quasi-isomorphic to the complex

$\ldots \to \epsilon _*\mathcal{J}^ n \to \epsilon _*\mathcal{J}^{n + 1} \to \frac{\epsilon _*\mathcal{J}^{n + 1} \oplus (\mathcal{K}')^{n + 2}}{(\mathcal{K}')^{n + 1}} \to (\mathcal{K}')^{n + 3} \to \ldots$

This finishes the induction step.

The induction procedure described above actually produces a sequence of quasi-isomorphisms of complexes

$(\mathcal{K}')^\bullet \to (\mathcal{K}'_{n_0})^\bullet \to (\mathcal{K}'_{n_0 + 1})^\bullet \to (\mathcal{K}'_{n_0 + 2})^\bullet \to \ldots$

where $(\mathcal{K}'_ n)^\bullet \to (\mathcal{K}'_{n + 1})^\bullet$ is an isomorphism in degrees $\leq n$ and such that $(\mathcal{K}'_ n)^ p = \epsilon _*\mathcal{J}^ p$ for $p \leq n$. Taking the “limit” of these maps therefore gives a quasi-isomorphism $(\mathcal{K}')^\bullet \to \epsilon _*\mathcal{J}^\bullet$ which proves the lemma. $\square$

Lemma 21.29.3. With $\epsilon : (\mathcal{C}_\tau , \mathcal{O}_\tau ) \to (\mathcal{C}_{\tau '}, \mathcal{O}_{\tau '})$ as above. Let

$\xymatrix{ E \ar[d] \ar[r] & Y \ar[d] \\ Z \ar[r] & X }$

be a commutative diagram in the category $\mathcal{C}$ such that

1. $h_ X^\# = h_ Y^\# \amalg _{h_ E^\# } h_ Z^\#$, and

2. $h_ E^\# \to h_ Y^\#$ is injective

where ${}^\#$ denotes $\tau$-sheafification. Then for $K' \in D(\mathcal{O}_{\tau '})$ in the essential image of $R\epsilon _*$ the map $c^{K'}_{X, Z, Y, E}$ of Lemma 21.26.1 (using the $\tau '$-topology) is an isomorphism.

Proof. This helper lemma is an almost immediate consequence of Lemma 21.26.3 and we strongly urge the reader skip the proof. Say $K' = R\epsilon _*K$. Choose a K-injective complex of $\mathcal{O}_\tau$-modules $\mathcal{J}^\bullet$ representing $K$. Then $\epsilon _*\mathcal{J}^\bullet$ is a K-injective complex of $\mathcal{O}_{\tau '}$-modules representing $K'$, see Lemma 21.21.9. Next,

$0 \to \mathcal{J}^\bullet (X) \xrightarrow {\alpha } \mathcal{J}^\bullet (Z) \oplus \mathcal{J}^\bullet (Y) \xrightarrow {\beta } \mathcal{J}^\bullet (E) \to 0$

is a short exact sequence of complexes of abelian groups, see Lemma 21.26.3 and its proof. Since this is the same as the sequence of complexes of abelian groups which is used to define $c^{K'}_{X, Z, Y, E}$, we conclude. $\square$

In your comment you can use Markdown and LaTeX style mathematics (enclose it like $\pi$). A preview option is available if you wish to see how it works out (just click on the eye in the toolbar).


text:
# Speed in Python¶

First, the good news: as a Data Scientist working in Python, most of the time whatever libraries you want to use have already been carefully engineered to deliver amazing performance, meaning working about code speed is something you usually won’t have to worry about. But understanding why programs like Python can sometimes be slow is still important for being able to avoid accidentally writing code that runs so slowly you can’t get your work done, and for trouble shooting if you end up in a situation where you really need something to go faster.

## The Python Ease of Use / Speed Tradeoff¶

There are two primary factors that determine the speed of a program:

• The number of computations computer has to complete (i.e. adding, multiplying, etc.)

• The amount it has to access and move data around (as discussed in What Is Big Data?, memory access is slow).

This is obviously kinda abstract, so let’s look at some real code and discuss what you computer is actually doing when it runs Python code. In particular, let’s focus on what happens in a loop like this:

summation = 0
for i in range(1000):
summation = summation + i

Now, you might think that all Python has to do to run this loop is add a bunch of numbers. But unfortunately, that’s not the case.

At each step of this loop, Python has to do the following:

1. Dereference summation (find the place in memory that is associated with the variable summation and read the data there)

2. Read that data to figure out the type of summation (in this case, it’s an integer).

3. Dereference i

4. Read that data to figure out the type of i (in this case, it’s an integer).

5. Lookup how it should interpret + given that summation is an integer and i is an integer.

• Remember: if summation and i were strings, it wouldn’t be doing addition, it would be concatenating! And because integers and floating point numbers are different things from the perspective of a computer, if i were an integer and summation were a floating point number, + would actually require (a) converting i to a floating point number, then (b) adding the floating point version of i to summation.

6. Compile low-level binary code (referred to as “machine code”) that can be read by the computer’s processor to tell it to execute an addition of two integers AND to also check and make sure that the operation won’t cause an integer overflow (remember: Python checks for integer overflows! That’s another operation!).

7. Run that code.

As you can see, there’s a lot going on in that simple line of code, and that process has to repeat every step of the loop.

Now, you might ask, is all of that necessary?

The answer is both yes and no. There are languages that don’t require all those steps (like C and C++, the standard-bearers for speed), but if Python didn’t do all those things when it ran, you wouldn’t be able to use Python the way you do.

Python is designed to be easy for you, the programmer. Unlike in some languages (like C), in Python you don’t have to declare that i is an integer explicitly in your code, and you are allowed to change i from an integer to a floating point number whenever you want. That makes Python what’s called a dynamically typed language, and it makes it very easy to use. If you wrote this in C, every time you made a new variable you’d have to declare it’s type. But the fact it’s dynamically typed means the language is never quite sure of the type of a variable until it explicitly checks that type, because it could change at any time.

Moreover, Python is a language you can use interactively. You can’t open a terminal and write and execute C code one line at a time. For languages like C (what are called “compiled languages”), you write all of your code, then hit compile, and your computer reads all your code and compiles low-level binary code for that entire program at once. Then the only way to use your C code is to run that compiled program. But the advantage of that is that step 6 (compiling your code) is done once in advance, and you don’t have to do that every time you run your code.

But to make Python interactive, it was decided that Python should evaluate each line of code when it reaches that code. That massively increases it’s flexibility and allows you to program interactively, but for loops like this, it means to do 1,000 additions, it also has to compile low-level machine code 1,000 times. (Note: there are newer languages like Julia that have are still interactive, but which are also smart enough to recognize these situations and only compile machine code once. Moreover, these languages also reduce the amount of “dereferencing” required. But that’s not Python.)

## Rules for Going Fast in Python¶

So now that you have some sense of why Python can be slow, let’s talk about how to keep your Python code fast (note to R users: basically everything I say here about Python also applies to R):

### Rule 1: Use other people’s functions¶

Let’s start with the dirty secret of Python: when you use a library in Python, the code you’re running was almost never actually written in Python. Instead, the functions you’re calling have a “thin” layer of Python at the top (which is what you’re interacting with), but when it comes to doing serious computations, the functions are actually calling tools written in C, which is blazing fast. (This is also true of R, by the way).

Thus the first rule of speed in Python: when you need speed, use tools that other people have written and distributed in big libraries (like pandas, sci-py, statsmodels, etc.). Because what you’re really doing is using C, and C is 10s or 100s of times faster than Python.

### Rule 2: Vectorize, Don’t write loops¶

When you use “vectorized” code (meaning code where you interact two full vectors or matrices in one command instead of looping over elements), you get huge performance gains. For example, consider the performance differences between the following two blocks of code, both of which do exactly the same thing:

[6]:

import numpy as np
numbers = np.arange(1000000)
numbers

[6]:

array([     0,      1,      2, ..., 999997, 999998, 999999])

[8]:

%%timeit
# Make a new array where each number is doubled
# done with a loop
b = numbers.copy()
for i in range(len(b)):
b[i] = numbers[i] * 2

357 ms ± 10.3 ms per loop (mean ± std. dev. of 7 runs, 1 loop each)

[10]:

%%timeit
# Now vectorized
b = numbers * 2

1.09 ms ± 40.6 µs per loop (mean ± std. dev. of 7 runs, 1000 loops each)

That’s a 300x speedup! For the exact same code!!!!

OK, so why does this happen?

First, when Python dereferences a variable (i.e. get the object associated with a variable), there are actually two steps to that process: first, Python must look up where to find the object in memory; then second it must go get the object.

Because Python evaluates every line of code when it reaches that line, in the loop example, in ever step of the loop Python has to look up where to find the array, then go get the array value.

But in the vectorized function, Python (or rather, the numpy code written in C that gets called) is designed to understand that it’s about to do something to every entry of an array, so it remembers where the array is located, and so only has to look up where to find the array once.

In addition, arrays are typed, meaning that Python also knows that every entry of the array it’s modifying is an integer. As a result, it doesn’t have to check the type of every entry in the array when the operation is vectorized, it checks once and knows that it’s working with an array of integers.

(You may say “but can’t it do the same in the loop?” In theory it could, and there are languages like Julia that are designed to be smarter about this kind of stuff. But currently, because Python only evaluates a line of code when it is reached means that it can be frustratingly myopic.)

### A Note On Object Vectors¶

You now also know enough to understand why object vectors in numpy and pandas are less performant.

When you’re working with a pandas Series or numpy array of integers, all of the entries of those arrays live in the same place in memory. This is because it is easy for a computer to put, say, 100 integers side by side, since it knows that each integer requires exactly 64 bits and so it can put them all end to end and tell the computer that each number starts 64 bits after the last.

But an object array is a little different. Instead of laying all the contents of the array in one place, an object array puts a collection of memory addresses in one place. This is because objects can be of arbitrary size, so you can’t put them all in one place in memory reliably. For example, suppose you had an array that had the following strings: 'this', 'is', 'an', 'array'. The first entry is longer than the second, is the same as the third, and is shorter than the third. You can’t just put them end-to-end and tell the computer “each number starts X bits after the last”.

But you can do that with memory addresses. So an object array is a collection of memory addresses (each the same size) laid end to end.

But that means that to look at the second entry of an object array, you have to go to the second location in the array, read the address, then go to that address. Moreover, because object arrays can hold anything, you could have an integer in the first entry, and a string in the second entry, so you can’t assume that when you see code like:

my_array * 2

that * will mean the same thing for each entry. In one entry, you might be doing integer multiplication; in another you might be doing floating point multiplication, in another you may be doubling up a list!

Indeed we can see this is we make a numpy object array full of ints and compare it to a numpy integer array. The both have the same content, but they are organized in memory differently:

[13]:

import numpy as np
object_numbers = np.array(np.arange(1000000),dtype='object')
numbers = np.arange(1000000)

[17]:

%timeit object_numbers * 2

27.6 ms ± 1.1 ms per loop (mean ± std. dev. of 7 runs, 10 loops each)

[18]:

%timeit numbers * 2

1.11 ms ± 49 µs per loop (mean ± std. dev. of 7 runs, 1000 loops each)

See? Same operation (doubling each entry of arrays with the integers from 0 to 1,000,000), but the object array operation is ~25x slower.

## Still have problems?¶

Check out more advanced performance solutions!


text:
# Another problem on Integration by parts

• February 8th 2010, 02:35 AM
confusedgirl
Another problem on Integration by parts
integrate e^x coshx dx
• February 8th 2010, 03:43 AM
jiboom
Quote:

Originally Posted by confusedgirl
integrate e^x coshx dx

if only you could write this as the integral of e^x[something involving e^x and e^(-x)]

This bit was only good to show 0=0 so no piont keeping it
• February 8th 2010, 04:01 AM
HallsofIvy
As jiboom suggested, the simplest thing to do is to use the definition of cosh(x) in terms of $e^x$. What are you using as the definition of cosh(x)?
• February 8th 2010, 04:03 AM
confusedgirl
(e^x + e^-x)/2
• February 8th 2010, 04:14 AM
confusedgirl
Quote:

Originally Posted by jiboom
if only you could write this as the integral of e^x[something involving e^x and e^(-x)]

or,if you have to do it by parts, just use parts twice. If we call the integral I., when you do parts twice you will end up with

I=something+kI whrer something and k are found from doing parts

which we can arrange as

(1-k)I=something

and so I can be found.

if i integrate by parts 2 times
the result will be I = 0/2 which is equal to zero
• February 8th 2010, 04:16 AM
Quote:

Originally Posted by confusedgirl
integrate e^x coshx dx

$Cosh(x)=\frac{e^x+e^{-x}}{2}$

$e^xCosh(x)=\frac{e^xe^x+e^xe^{-x}}{2}=\frac{e^{2x}+e^0}{2}$

$=\frac{e^{2x}+1}{2}$

$\frac{1}{2}\int{e^{2x}}dx+\int{\frac{1}{2}}dx=\fra c{1}{2}\int{e^xe^x}dx+\frac{x}{2}+C$

To integrate by parts

Let $\int{e^xe^x}dx=I$

$u=e^x\ \Rightarrow\ du=e^xdx$

$dv=e^xdx\ \Rightarrow\ v=e^x$

$uv-\int{v}du=e^xe^x-\int{e^xe^x}dx$

$I=e^{2x}-I$

$2I=e^{2x}$

$I=\frac{e^{2x}}{2}+C$

Therefore

$\int{e^xCosh(x)}dx=\frac{1}{4}e^{2x}+\frac{1}{2}x+ C$
• February 8th 2010, 08:50 AM
jiboom
Quote:

Originally Posted by confusedgirl
if i integrate by parts 2 times
the result will be I = 0/2 which is equal to zero

(Blush)(Blush)(Blush)(Blush)(Blush)(Blush)

i only added that as an edit as you wanted parts. I have never done that sort of integral by parts, i would use my first (and useful comment).


text:
# reaction of metals with acids experiment

When the air in a specific area contains moisture mixed with acid or salt, we refer to the area as having a _____ climate. Place about 5cm depth of the acid in each of the five test tubes; Place a small piece of each of the three metals above. This is an example of a single displacement reaction. The reaction is similar to the reaction with water, forming the metal salt (either sulfate or chloride) plus H 2(g).. For example. Describe the test for hydrogen. Acids and metals ; Acids and carbonates ; Acids and hydroxides ; Acids and Metals. EXPERIMENT S: Periodicity: Reactions of Metals with Acids 4. This is the currently selected item. Mn(s) + CuSO 4(aq) → MnSO 4(aq) + Cu(s) Metal carbonates such as calcium carbonate (chalk) react with acids to produce the gas carbon dioxide. Describe patterns and trends in results. All the metals react with dilute hydrochloric acid to give bubbles of hydrogen and a colourless solution of the metal chloride. The Reaction of Metals with Dilute Acid.. Potassium, sodium, lithium and calcium all react violently with dilute sulfuric acid and dilute hydrochloric acid. The gradual destruction of materials (usually metals) by chemical reaction with the environment is called _____. Table of Contents. Scientific report includes Aim, Hypothesis, Apparatus, Method, Discussion and Conclusion. Active metals react with acids to produce hydrogen gas and a salt. This page looks at the reactions of the Group 2 elements - beryllium, magnesium, calcium, strontium and barium - with common acids. The experiment reinforces ideas about energy changes during reactions, the reactivity series of the metals, and the chemical behaviour of acids. The product of the reaction between a metal and oxygen is called a _____. The following table shows the reaction of metals in oxygen, water and acid. Step by step experiment investigating the reaction of acids & metals, and acids & carbonates. Experiment 2A – Reaction of Acid and Base. This set of differentiated Reactions of Acids homework worksheets helps enable your students to practice naming the salts made when metals are reacted with acids. Reactivity of Metals Experiment. The carbon dioxide produced can be tested for in the lab using limewater, which reacts with the carbon dioxide gas. CuO + H 2 SO 4 – CuSO 4 + H 2 O. Acids react with metallic oxides to give salt and water similar to the reaction acid … It is known that the course of reaction of metals with acids depends on various conditions 3.For example, in the absence of oxygen under real conditions copper does not react with hydrochloric acid and dilute sulfuric acid, what is indicated by the value of EMF. Rusting is an example of a process called corrosion. All you need is a selection of metals, dilute hydrochloric acids, rack of test tubes and a splint. The acids will either be hydrochloric, ethanoic, sulphuric or phosphoric acid. Record observations and evidence systematically. acids and metals - View presentation slides online. Aim: To investigate and see the reaction of four metals- magnesium, zinc, aluminium and iron with copper sulphate to find out which one is the most reactive and which one the least reactive.. Reactions with dilute hydrochloric acid. Experiment : reaction of metals with mineral acids. Lead and the metals ranking above lead on the activity series form salts when reacted with hydrochloric acid or sulphuric acid. Donate or volunteer today! Next lesson. It is dangerous to put these metals into an acid. INTRODUCTION. Spectator ions are ions in a chemical reaction that aren't really involved in the reaction. Reaction of Acids and Bases with Metals Let's perform a very interesting experiment Take 5 mL of sulphuric acid in a test tube and add a few pieces of zinc granules to it. Reaction of metal and acid Single displacement reaction between magnesium and hydrochloric acid produce magnesium chloride and hydrogen gas. For example: $Mg + H_2SO_4 \rightarrow MgSO_4 + H_2$ AIM OF THE EXPERIMENT Understanding that metals react with acid to produce salt and hydrogen, Understanding how the reactivity series of metals can be determined by considering the reaction of metals with acids. Acids and Bases React with Metals. Khan Academy is a 501(c)(3) nonprofit organization. When acid reacts with metallic oxide then it forms corresponding salt and water. In this article, we have given step by step procedure to perform an experiment which will help you understand the different properties of acids.Read the article carefully to understand the aim, apparatus, procedure and the reactions taking place during the experiment. Acids react with most metals to form a salt and hydrogen gas. Lesson organisation. What is produced by the action of acids with active metals? The Reactivity Series. The first group of reactions we'll discuss is when a metal and an acid are combined. Test for … Site Navigation. Reactions Cu with acids at different conditions. After exposure to oxygen in the air, both magnesum and aluminum become covered by a thin film of oxide. Reaction of Non- metals with acids. The reaction between zinc and sulphuric acid is an example of such a reaction. Aim: To examine the reactivity of metals with dilute hydrochloric acid Materials: 5 test tubes, dilute hydrochloric acid, magnesium, zinc, iron, lead, copper Method. Practice: Metals reacting with air and water. These reactions also involve the liberation of hydrogen gas. (a)Place 5cm3 of dilute hydrochloric acid in a small test tube. Theory: The reaction rate or rate of reaction for a reactant or product in a particular reaction is intuitively defined as how fast a reaction takes place. With both higher and lower ability worksheets available in this pack, you can tailor the tasks to your students and make sure they're getting the support and reinforcement they need. Hydrogen gas is formed, along with colorless solutions of beryllium or magnesium sulfate. Reaction of Acid and Base Reaction of Base with a Metal. Metal oxide + acid – salt + water. ... Open navigation menu The hydrochloric acid used in this experiment is relatively concentrated, and the temperature rises can be quite significant. Reaction Between Metals and Acids. Example 3: In this example a metal is combined with a solution of a metal salt. Space provided for students to fill out missing information, their results, and answer the discussion questions provided. Scroll down the page for examples and solutions. You might have to leave the metals that react too slowly until the next lesson; For metals such as calcium that react quickly with water set up the apparatus shown above so that you can collect the hydrogen gas that is given off during the reaction; Test the collected gas using a glowing splint The metals at the bottom of the reactivity series will react slowly or will not react with water and dilute acids as they are less reactive Reaction with Water The table below shows how the metals from the reactivity series react with Water: Non-metals tend to gain electrons when they react. The resource is set out as teachers' notes followed by the students' page which presents the task to be investigated. Filed Under: Class 8, Material:Metals and Non-metals Tagged With: Reaction of Aluminium with HCl, reaction of iron with HCl, reaction of magnesium with HCl, reaction of metal with acid. These metals react with with dilute sulfuric acid just as they did with dilute hydrochloric acid; the reaction between magnesium and dilute sulfuric is familiar to many beginning chemists. Reactivity series. Observe the reactions of the metals with water. Students conduct an experiment to test the reactivity of metals and non-metals. Corrosion means that a chemical reaction has occurred in which metal atoms have combined with oxygen to form an oxide coat. When those metal atoms are iron, the corrosion is "bad," because it corrodes quickly, weakening the original steel material. Metals (be sure you can locate them on the periodic table) tend to react by losing one or more electrons (per atom). This can be seen in the equation: Metal carbonate + Acid Salt + Water + Carbon dioxide. They do not react with dilute acids to form salt and hydrogen gas. Reaction of metallic oxides with acids . The general equation of this type of chemical reaction is. REPORT SHEET EXPERIMENT Activity Series 10 A. The Reaction of Metals with Hydrochloric Acid. Lab Session 6, Experiment 5: Hydrogen and the Activity Series of Metals An activity series is a listing of chemical species in order of increasing (or decreasing) reactivity. These metals took longer to react because the acid had to react with the oxides first. Metals reacting with air and water. Active metal + acid salt + hydrogen gas. When the air pollutants, NO x and SO 2, react with moisture in the atmosphere, "acid rain" is produced.Organic and inorganic acids make up … Results and Discussion 2.1. In this chemistry lesson students test metals with different chemicals to observe the reaction. Reactions of Metals with Acid Reaction Metalwith HCI Observation Equationsi Ca2 Cu Mg verslos reaction Fe Nes (S Sn reachon Zn S IDw Example: Yes, slowly Gas evolved; solution Co turned blue CHEM L110 - Chemistry and Society Laboratory Experiment #7 Reaction of Acids with Metals and Other Substances. 2. The Rate of Reaction Of Metals with Acids Introduction In this investigation I will be looking at the rate of reaction between a metal, which will be magnesium ribbon, and an acid. Some metals, like Hg do not react with acids, for example: Hg(l) + HCl → No Reaction, so the Hg is less active than hydrogen. Fair test points: Ideally all the metals would be in the same physical state, other than all being solids. As discussed previously, metals that are more active than acids can undergo a single displacement reaction.For example, zinc metal reacts with hydrochloric acid, producing zinc chloride and hydrogen gas. Metal + Acid -> Salt + Hydrogen gas . All acids react with a reactive metals to form a salt and produce /evolve hydrogen gas. Our mission is to provide a free, world-class education to anyone, anywhere. Add 1cm length of polished magnesium ribbon. In this microscale chemistry experiment, from the Royal Society of Chemistry, students observe the reactions between metals and different acids using a worksheet covered by a clear plastic sheet. The results are used to categorize the metals. Reaction with metals. Metals reacting with acid.


text:
# Using data files with statistical and mathematical software on IUanyWare

When using local data files (i.e., files on a disk drive, such as a computer hard disk or flash drive) on IUanyWare, you need to point the IUanyWare program to your local (client) machine. With programs that use graphical user interfaces, you can do this by finding the appropriate computer and directory in the "Open" dialog box in the File menu (see When I use an IUanyWare application, how do I save my files?).

In other software packages that require syntax (or have the option of using syntax), you may be required to type a path to access a file. See the following syntax examples for the specific application you are using.

Each software section lists three examples: one to read in a software-specific file (or library), one to import a Microsoft Excel file, and one to read in a tab-delimited text file (with three variables and variable names in the first row). All examples are set up such that the desired files are in the hard disk location of C:\Temp; be sure to customize your locations and commands as necessary for your specific file.

Note:
Due to compatibility issues between 64-bit and 32-bit Excel files, we recommend that you save Excel files as CSV files if you find errors importing Excel files.

## Mac

The above examples will work on a Mac when you put your files in the Temp folder in your home directory (e.g., /Users/<username>/Temp). If your files are on the desktop, you can change the path to \\Client\C$\Users\<username>\Desktop\. For example, to read an Excel file to Stata, the code becomes:  import excel "\\Client\C$\Users\<username>\Desktop\test.xlsx", clear

By default, the path \\Client\C\$\ points to the home directory on your Mac unless you have configured it otherwise. You will need to structure your file path accordingly.

If you have questions about using statistical and mathematical software at Indiana University, contact Research Analytics. Research Analytics is located on the IU Bloomington campus at Woodburn Hall 200; staff are available for consultation Monday-Friday 9am-noon and by appointment.

This is document bbtr in the Knowledge Base.

#### I need help with a computing problem

• Fill out this form to submit your issue to the UITS Support Center.
• Please note that you must be affiliated with Indiana University to receive support.
• All fields are required.

Please provide your IU email address. If you currently have a problem receiving email at your IU account, enter an alternate email address.

#### I have a comment for the Knowledge Base

• Fill out this form to submit your comment to the IU Knowledge Base.
• If you are affiliated with Indiana University and need help with a computing problem, please use the I need help with a computing problem section above, or contact your campus Support Center.

Please provide your IU email address. If you currently have a problem receiving email at your IU account, enter an alternate email address.

Version: trunk


text:
# Cheap alternative to an accelerometer [closed]

I am designing a very simple device, which absolutely needs to be inexpensive, total BOM cost < $1.00 including the MCU (at 10k+ units). This device would benefit from knowing its orientation, which could be binary - vertical / non-vertical. I do not need the granularity of an accelerometer just a reliable way to determine single axis position in a binary format. After a google search, I am still empty handed, I have only been able to find full blown accelerometers which start at around$0.40. I was hoping to get something fo \$0.10 or less (at quantity). I would love to get some input on any options for this.

## closed as off-topic by Voltage Spike, uint128_t, Nick Alexeev♦Mar 3 '17 at 4:30

This question appears to be off-topic. The users who voted to close gave this specific reason:

If this question can be reworded to fit the rules in the help center, please edit the question.

• Can you use a ball tilt switch? – Chris Stratton Mar 2 '17 at 5:39
• Um, can you tell me where you are finding accelerometers for only 40 cents? :) – bitsmack Mar 2 '17 at 6:36


text:
# Difference between revisions of "2006 USAMO Problems"

## Day 1

### Problem 1

Let $p$ be a prime number and let $s$ be an integer with $0 < s < p$. Prove that there exists integers $m$ and $n$ with $0 < m < n < p$ and

{$\frac{sm}{p}$} < {$\frac{sn}{p}$}< ${\frac{s}{p}}$

if and only if $s$ is not a divisor of $p-1$.

Note: For $x$ a real number, let $\lfloor x \rfloor$ denote the greatest integer less than or equal to $x$, and let $\{x\} = x - \lfloor x \rfloor$ denote the fractional part of x.

### Problem 2

For a given positive integer k find, in terms of k, the minimum value of $N$ for which there is a set of $2k+1$ distinct positive integers that has sum greater than $N$ but every subset of size k has sum at most $\frac{N}{2}$.

### Problem 3

For integral $m$, let $p(m)$ be the greatest prime divisor of $m$. By convention, we set $p(\pm 1)=1$ and $p(0)=\infty$. Find all polynomial $f$ with integer coefficients such that the sequence

$(p(f(n^2))-2n)_{n\ge 0}$

is bounded above. (In particular, this requires $f(n^2)\neq 0$ for $n\ge 0$


text:
2.3: Powers of Trig Functions

\begin{align} \int \sin^5 x \, dx &= \int \sin^4 x \, \sin x \, dx \\ &= \int (\sin^2 x)^2 \sin x \,dx \\ &= \int (1-\cos^2x)^2 \sin x \, dx \\ &\text{substitute } u = \cos x \text{ and } du = -\sin x\, dx \\ &= -\int (1 - u^2)^2 du \\ & = -\int [1 - 2u^2 + u^4] \; du \\ &= -u + \dfrac{2}{3} u^3 - \dfrac{1}{5} u^5 + C \\ &= -\cos x + \dfrac{2}{3} \cos^3 x - \dfrac{1}{5} \cos^5x + C \end{align}.

Evaluate $$\int \cos^7 x \, dx$$.

Evaluate $$\int \sin^4 x\, dx$$.

Solution

We write

\begin{align} \int \sin^4 x \; dx &= \int (\sin^2 x)^2 dx \\ &= \int \Big(\dfrac{1}{2} - \dfrac{1}{2} \cos(2x)\Big)^2 \; dx \\ &= \int \Big[ \dfrac{1}{4}-\dfrac{1}{2} \cos(2x) + \dfrac{1}{4} \cos^2(2x) \Big] dx \end{align}

For the second integral let $$u = 2x$$ and $$dx = \dfrac{1}{2} du$$.

The integral becomes

$\dfrac{1}{4} x - \dfrac{1}{4} \sin(2x) + \dfrac{1}{4}\int \Big[ \dfrac{1}{2}+\dfrac{1}{2} \cos(4x) \Big] dx$

$\text{Let } u = 4x, dx = \dfrac{1}{4} \; du$

$\dfrac{1}{4}x - \dfrac{1}{4}\sin(2x) +\dfrac{1}{8}x +\dfrac{1}{32}\sin(4x) +C.$

We see that if the power is odd we can pull out one of the sin functions and convert the other to an expression involving the cos function only. Then use $$u = \cos x.$$

If the power is even, we must use the trig identities

$\sin^2x = \dfrac{1}{2} - \dfrac{1}{2} \cos (2x)$

and

$\cos^2 x = \dfrac{1}{2} + \dfrac{1}{2} \cos (2x).$

This method will always work and is always long and tedious.

\begin{align} \int u^2 (1-u^2) \; du &= \int u^2-u^4 \; du \\ &= \dfrac{1}{3}u^5 + C \\ &= \dfrac{1}{3} \sin^3 x -\dfrac{1}{5} \sin^5 x + C \end{align}

$\int \sin^5 x \cos^2 x \, dx$

Powers of Tangents and Secants

To integrate powers of tangents and secants we use the formula

$\tan^2 x = \sec^2 x - 1.$

\begin{align} \int u^2 \,du - \tan x + x &= \dfrac{1}{3} u^3 - \tan x + x + C \\ &= \dfrac{1}{3} \tan^3 x - \tan x + x + C \end{align}.

$\int \sec^5 x \tan^3 x \, dx.$

Mixed Angles

We have the following formulas:

$\sin(m \theta) \sin(n \theta) = \dfrac{1}{2} \left[ \cos[(m - n) \theta] - \cos[(m + n) \theta] \right]$

$\sin(m \theta) \cos(n \theta) = \dfrac{1}{2} \left[ \sin[(m - n) \theta] + \sin[(m + n) \theta] \right]$

$\cos(m \theta) \cos(n \theta) = \dfrac{1}{2} \left[ \cos[(m - n) \theta] + \cos[(m + n) \theta] \right].$

$\dfrac{1}{2} -\sin{(-x)} + \dfrac{1}{7} \sin{(7x)} + C.$

Larry Green (Lake Tahoe Community College)

• Integrated by Justin Marshall.


text:
# HSC Chemistry Module 6: Acid and Base Reactions Question Sets

Regular price
$19.99 Sale price$19.99
Tax included.

Module 6: Acid and Base Reactions Question Sets contains 5 booklets, each consisting of MCQs and extended response questions that are created to help students consolidate their knowledge throughout the module. Each booklet is tailored to the content of each of the 5 sections in Module 6: Acid and Base Reactions Notes.

Answers (MCQ key and High Band 6 answers to Extended Response Questions) are included in the purchase.


text:
## LaTeX forum ⇒ Graphics, Figures & Tables ⇒ How to change the frame line thickness ? Topic is solved

Information and discussion about graphics, figures & tables in LaTeX documents.
Cham
Posts: 830
Joined: Sat Apr 02, 2011 4:06 pm

### How to change the frame line thickness ?

I don't need anything fancy. Just to change the frame thickness in this MWE example :

\documentclass[12pt,letterpaper,twoside]{book}\usepackage{lmodern}\usepackage{amsmath}\usepackage{graphicx} \begin{document} 	\begin{figure}		\centering		\frame{\includegraphics[height=6.5cm]{example-image}}	\end{figure} \end{document}

If possible, I don't want to use another package just to change the line thickness. Any suggestion ? Are there some options for the \frame command ?

Johannes_B
Site Moderator
Posts: 3644
Joined: Thu Nov 01, 2012 4:08 pm
Better use fbox.
\documentclass[12pt,letterpaper,twoside]{book}\usepackage{lmodern}\usepackage{amsmath}\usepackage{graphicx} \begin{document} \begin{figure}\centering\setlength{\fboxrule}{5pt}\setlength{\fboxsep}{0pt}\fbox{\includegraphics[height=6.5cm]{example-image}}\end{figure}\begin{figure}\centering\makeatletter\@wholewidth5pt\makeatother\frame{\includegraphics[height=6.5cm]{example-image}}\end{figure} \end{document}
The smart way: Calm down and take a deep breath, read posts and provided links attentively, try to understand and ask if necessary.

Cham
Posts: 830
Joined: Sat Apr 02, 2011 4:06 pm
Indeed, fbox appears to solve my issue. Thanks a lot !


text:
# Upper bounds for the solution of an elliptic PDE depending on a parameter.

Suppose I have the following PDE on $[0,1]^n$ $$\mathcal{L}u = -\nabla \cdot \left(a(x, r)\nabla u\right) = f(x,r), \qquad x\in [0,1]^n,$$ with periodic boundary conditions and $\int f(x) dx =0$ . Suppose that $a_{ij} \in C^\infty([0,1]^n \times \mathbb{R})$, and that for fixed $r \in \mathbb{R}$, $$0 < \lambda(r)|z|^2 \leq z\cdot a(x,r)z \leq \Lambda(r)|z|^2, \quad z \in \mathbb{R}^n,$$ for some smooth functions $\lambda(\cdot)$ and $\Lambda(\cdot)$.

Thus for fixed $r$ we can apply Lax-Milgram to give us the existence of a unique solution $u$ with $\int_{[0,1]^n} u(x) \,dx = 0$. Now, it is straightforward to show that $$||u(\cdot, r)||^2_{H^1} \leq \frac{C}{\lambda(r)}||f(\cdot, r)||^2_{L^2},$$ where $C$ depends only on $n$.

One can similarly derive $L^{\infty}$ bounds for $u$, however, I have not been able to see how the constants in these bounds depend on $r$. I am interested to see how these bounds grow with varying $r$. So my question is the following:

It is possible to derive similar upper bounds on $||u||_{L^{\infty}}$ as a function of $r$, where the upper bounds can be expressed explicitly? Of course, the bounds needn't be tight.

-
It seems to me what you are asking is the same as to use elliptic regularity theory (there are several flavors that work with coefficients as smooth as you have provided) to provide a modulus of continuity for your function. Since your function $u$ has average 0, a continuous version of $u$ must be 0 at some point, and thus is bounded in magnitude by the modulus of continuity. If you pay attention to how that modulus changes with respect to the ellipticity of the equation (" $\lambda(r)$ ") and the norm of your source term $f$, then you have what you desire. –  Ray Yang Feb 3 '13 at 0:39
One rough idea is to take whatever estimates we have for $\Delta v = f$ and "reduce to this case" with the rescalings $\tilde{u}(x) = u(Ax)$ for some affine transformation $A$. Of course, when $a$ depends on $x$ this won't necessarily help the ellipticity at all points (it only works for constant coefficients) but it might give some insights. Otherwise, just look at the proofs and track explicitly the dependence on $\lambda,\Lambda$ at each step. –  Connor Mooney Sep 18 '13 at 3:07

Is the general $n$-dimensional case important?

With $n\leq3$, it can be done with off the shelf estimates. The following estimate can be proved using the De Giorgi-Nash-Moser method: If $a_{i,j} \xi_i \xi_j \geq 1$ (and in $L^\infty$) then the solution in $H^1_0(B_1)$ of $$-\textrm{div}(a \nabla u) + u \leq f + div(g)$$ with $f\in L^p$ and $g \in L^{2p}$ and $p>n/2$ satisfies $$\| u\|_{L^\infty(B_1)} \leq C(n,p) ( \|f\|_{L^p(B_1)} + \|g\|_{L^{2p}(B_1)})$$
To go from your case to this one,

1. Change $a \to a/\lambda(r)$ and $f \to f/\lambda(r)$

2. Add +u to both sides.

At this point, you would are almost done since your right hand-side is $L^2$ and $2>3/2$. Your solution is not in $H^1_0(B_1)$ so you add a cut-off:

1. you consider instead $u\times \chi$ with an explicit smooth $\chi$ of your choice supported in $B_1$ equal to $1$ in $B_{1/2}$.

This adds to the right-hand side two terms (I think), $$2 a \nabla \chi \cdot \nabla u + \textrm{div}(a \nabla \chi ) u$$ and these terms are still in $L^2$ with bounds depending on the $C^1$ norm of $a$ for example, since you already have an $H^1$ bound.

And you are done, covering your box with a few boxes (4 maybe), the result is explicit: $$\| u\|_{L^\infty} \leq C(n) \frac{1+\sqrt{\Lambda(r)}+\|\nabla a\|_{L^{\infty}}}{\sqrt{\lambda(r)}} \|f\|_{L^2}$$ (you can lower the $L^\infty$ bound to a $L^3$ if it helps) If you want to use the same idea for bigger $n$, you need to derive $W^{n,p}$ estimates for $u$ and use that instead (replacing $f$ by div$(a \nabla u)$!). But that becomes just as bad as tracking constants in De Giorgi-Nash-Moser directly.

-


text:
# Firefox – Stop Firefox’s Session Restore from Loading All the Tabs at Once

browser-tabsfirefoxfirefox-extensions

When I use Firefox I often have many tabs and many windows open (even more so now that they have panorama). I often use the session restore feature because I don't want to loose all my open windows when installing a new add on or restarting my computer for updates. However, with so many tabs open it takes a really, really long time for Firefox to load all the tabs. I'm looking for an extension that will open a place holder tab for all of the websites on session restore but won't actually load the page until I click on that tab to bring it to focus. Basically it would like like I had 40 tabs open but until I click on that tab it won't be taking up any more memory than an about:blank page.

Another more reliable way is to use the new about:config property, browser.sessionstore.max_concurrent_tabs.
Go to about:config in firefox and search for browser.sessionstore.max_concurrent_tabs. Set the integer value to 0.