Index: kernel/arch/abs32le/include/atomic.h =================================================================== --- kernel/arch/abs32le/include/atomic.h (revision e821e497bdb3d07036342b84204a38ccc7f2bc09) +++ kernel/arch/abs32le/include/atomic.h (revision 09a0bd4a4ab5a70550f327984b135164b05aa58d) @@ -39,6 +39,9 @@ #include #include +#include -static inline void atomic_inc(atomic_t *val) { +ATOMIC static inline void atomic_inc(atomic_t *val) + REQUIRES(val->count < ATOMIC_COUNT_MAX) +{ /* On real hardware the increment has to be done as an atomic action. */ @@ -47,12 +50,15 @@ } -static inline void atomic_dec(atomic_t *val) { +ATOMIC static inline void atomic_dec(atomic_t *val) + REQUIRES(val->count > ATOMIC_COUNT_MIN) +{ /* On real hardware the decrement has to be done as an atomic action. */ - val->count++; + val->count--; } -static inline atomic_count_t atomic_postinc(atomic_t *val) +ATOMIC static inline atomic_count_t atomic_postinc(atomic_t *val) + REQUIRES(val->count < ATOMIC_COUNT_MAX) { /* On real hardware both the storing of the previous @@ -66,5 +72,6 @@ } -static inline atomic_count_t atomic_postdec(atomic_t *val) +ATOMIC static inline atomic_count_t atomic_postdec(atomic_t *val) + REQUIRES(val->count > ATOMIC_COUNT_MIN) { /* On real hardware both the storing of the previous @@ -81,6 +88,10 @@ #define atomic_predec(val) (atomic_postdec(val) - 1) -static inline atomic_count_t test_and_set(atomic_t *val) +ATOMIC static inline atomic_count_t test_and_set(atomic_t *val) { + /* On real hardware the retrieving of the original + value and storing 1 have to be done as a single + atomic action. */ + atomic_count_t prev = val->count; val->count = 1; @@ -88,8 +99,18 @@ } +ATOMIC static inline atomic_count_t arch_atomic_get(atomic_t *val) +{ + /* This function is not needed on real hardware, it just + duplicates the functionality of atomic_get(). It is + defined here because atomic_get() is an inline function + declared in a header file which we are included in. */ + + return val->count; +} + static inline void atomic_lock_arch(atomic_t *val) { do { - while (val->count); + while (arch_atomic_get(val)); } while (test_and_set(val)); } Index: kernel/arch/abs32le/include/types.h =================================================================== --- kernel/arch/abs32le/include/types.h (revision e821e497bdb3d07036342b84204a38ccc7f2bc09) +++ kernel/arch/abs32le/include/types.h (revision 09a0bd4a4ab5a70550f327984b135164b05aa58d) @@ -35,4 +35,7 @@ #ifndef KERN_abs32le_TYPES_H_ #define KERN_abs32le_TYPES_H_ + +#define ATOMIC_COUNT_MIN UINT32_MIN +#define ATOMIC_COUNT_MAX UINT32_MAX typedef uint32_t size_t; Index: kernel/generic/include/atomic.h =================================================================== --- kernel/generic/include/atomic.h (revision e821e497bdb3d07036342b84204a38ccc7f2bc09) +++ kernel/generic/include/atomic.h (revision 09a0bd4a4ab5a70550f327984b135164b05aa58d) @@ -38,11 +38,12 @@ #include #include +#include -static inline void atomic_set(atomic_t *val, atomic_count_t i) +ATOMIC static inline void atomic_set(atomic_t *val, atomic_count_t i) { val->count = i; } -static inline atomic_count_t atomic_get(atomic_t *val) +ATOMIC static inline atomic_count_t atomic_get(atomic_t *val) { return val->count; Index: kernel/generic/include/verify.h =================================================================== --- kernel/generic/include/verify.h (revision 09a0bd4a4ab5a70550f327984b135164b05aa58d) +++ kernel/generic/include/verify.h (revision 09a0bd4a4ab5a70550f327984b135164b05aa58d) @@ -0,0 +1,55 @@ +/* + * Copyright (c) 2010 Martin Decky + * All rights reserved. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions + * are met: + * + * - Redistributions of source code must retain the above copyright + * notice, this list of conditions and the following disclaimer. + * - Redistributions in binary form must reproduce the above copyright + * notice, this list of conditions and the following disclaimer in the + * documentation and/or other materials provided with the distribution. + * - The name of the author may not be used to endorse or promote products + * derived from this software without specific prior written permission. + * + * THIS SOFTWARE IS PROVIDED BY THE AUTHOR ``AS IS'' AND ANY EXPRESS OR + * IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES + * OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. + * IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY DIRECT, INDIRECT, + * INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT + * NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, + * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY + * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT + * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF + * THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + */ + +/** @addtogroup genericverify + * @{ + */ +/** @file + */ + +#ifndef KERN_VERIFY_H_ +#define KERN_VERIFY_H_ + + +#ifdef CONFIG_VERIFY_VCC + +#define ATOMIC __spec_attr("atomic_inline", "") +#define REQUIRES(...) __requires(__VA_ARGS__) + +#else /* CONFIG_VERIFY_VCC */ + +#define ATOMIC +#define REQUIRES(...) + +#endif /* CONFIG_VERIFY_VCC */ + + +#endif + +/** @} + */ Index: tools/checkers/vcc.py =================================================================== --- tools/checkers/vcc.py (revision e821e497bdb3d07036342b84204a38ccc7f2bc09) +++ tools/checkers/vcc.py (revision 09a0bd4a4ab5a70550f327984b135164b05aa58d) @@ -59,5 +59,5 @@ args = ['gcc', '-E'] args.extend(options.split()) - args.append(srcfname) + args.extend(['-DCONFIG_VERIFY_VCC=1', srcfname]) # Change working directory @@ -69,4 +69,10 @@ tmpf = file(tmpfname, "w") + + tmpf.write("__specification(const char * const \\declspec_atomic_inline;)\n\n"); + + tmpf.write("#define __spec_attr(key, value) \\\n"); + tmpf.write(" __declspec(System.Diagnostics.Contracts.CodeContract.StringVccAttr, \\\n"); + tmpf.write(" key, value)\n\n"); for line in preproc.splitlines(): @@ -149,5 +155,5 @@ # Run Vcc print " -- %s --" % srcfname - retval = subprocess.Popen([vcc_path, cygpath(tmpfqname)]).wait() + retval = subprocess.Popen([vcc_path, '/pointersize:32', cygpath(tmpfqname)]).wait() if (retval != 0):