Getting SharC to check some locking
authorZach Anderson <zra@zra-intrepid.(none)>
Fri, 28 Aug 2009 19:49:24 +0000 (12:49 -0700)
committerZach Anderson <zra@zra-intrepid.(none)>
Fri, 28 Aug 2009 19:49:24 +0000 (12:49 -0700)
57 files changed:
GNUmakefile
kern/Makefrag
kern/arch/i386/apic.c
kern/arch/i386/arch.h
kern/arch/i386/atomic.h
kern/arch/i386/colored_caches.c
kern/arch/i386/console.c
kern/arch/i386/cpuinfo.c
kern/arch/i386/env.c
kern/arch/i386/kclock.c
kern/arch/i386/kdebug.c
kern/arch/i386/page_alloc.c
kern/arch/i386/pmap.c
kern/arch/i386/smp.c
kern/arch/i386/smp_boot.c
kern/arch/i386/trap.c
kern/arch/sparc/env.c
kern/arch/sparc/pmap.c
kern/arch/sparc/trap.c
kern/include/assert.h
kern/include/atomic.h
kern/include/env.h
kern/include/ivy/sharc.h [new file with mode: 0644]
kern/include/monitor.h
kern/include/pmap.h
kern/include/process.h
kern/include/ros/memlayout.h
kern/include/stdio.h
kern/include/syscall.h
kern/include/trap.h
kern/ivy/Makefrag
kern/ivy/deputy.c
kern/ivy/sharc.c [new file with mode: 0644]
kern/src/atomic.c
kern/src/colored_caches.c
kern/src/env.c
kern/src/init.c
kern/src/kfs.c
kern/src/kmalloc.c
kern/src/manager.c
kern/src/monitor.c
kern/src/multiboot.c
kern/src/page_alloc.c
kern/src/pmap.c
kern/src/printf.c
kern/src/printfmt.c
kern/src/process.c
kern/src/readline.c
kern/src/schedule.c
kern/src/smp.c
kern/src/string.c
kern/src/syscall.c
kern/src/sysevent.c
kern/src/testing.c
kern/src/timer.c
kern/src/workqueue.c
user/Makefrag

index c1a7291..2c9e79f 100644 (file)
@@ -20,6 +20,7 @@ TARGET_ARCH := i386
 TOP_DIR := .
 ARCH_DIR := $(TOP_DIR)/kern/arch
 INCLUDE_DIR := $(TOP_DIR)/kern/include
+
 UNAME=$(shell uname -m)
 V = @
 
@@ -48,7 +49,15 @@ GCCPREFIX := $(shell if i386-ros-elf-objdump -i 2>&1 | grep '^elf32-i386$$' >/de
 endif
 
 # Default programs for compilation
-CC         := ivycc --deputy --gcc=$(GCCPREFIX)gcc --enable-error-db $(EXTRAARGS)
+KERN_IVY_FLAGS := --deputy\
+                  --enable-error-db\
+                  --no-rc-sharc\
+                  --sc-dynamic-is-error\
+                  --sc-ops=$(INCLUDE_DIR)/ivy/sharc.h\
+                  --sc-all-in-thread
+                  $(EXTRAARGS)
+USER_IVY_FLAGS := --deputy --enable-error-db $(EXTRAARGS)
+CC         := ivycc --gcc=$(GCCPREFIX)gcc
 AS         := $(GCCPREFIX)as
 AR         := $(GCCPREFIX)ar
 LD         := $(GCCPREFIX)ld
index 3687d72..39c72cd 100644 (file)
@@ -1,6 +1,6 @@
 KERN_DIR := kern
 
-KERN_CFLAGS := $(CFLAGS) -DROS_KERNEL
+KERN_CFLAGS := $(KERN_IVY_FLAGS) $(CFLAGS) -DROS_KERNEL
 KERN_CFLAGS += -I$(INCLUDE_DIR)
 KERN_LDFLAGS := $(LDFLAGS)
 
index 6cc68f6..c5a465a 100644 (file)
@@ -4,6 +4,10 @@
  * See LICENSE for details.
  */
 
+#ifdef __SHARC__
+#pragma nosharc
+#endif
+
 #include <arch/mmu.h>
 #include <arch/x86.h>
 #include <arch/arch.h>
index 135dedc..448a8eb 100644 (file)
@@ -135,7 +135,7 @@ irq_is_enabled(void)
 }
 
 static __inline uint32_t
-core_id(void)
+( core_id)(void)
 {
        return lapic_get_id();
 }
index 3dbfa75..3e7d651 100644 (file)
@@ -16,8 +16,8 @@ static inline void atomic_set(atomic_t *number, int32_t val);
 static inline void atomic_inc(atomic_t *number);
 static inline void atomic_dec(atomic_t *number);
 static inline void atomic_andb(volatile uint8_t* number, uint8_t mask);
-static inline void spin_lock(volatile uint32_t*COUNT(1) lock);
-static inline void spin_unlock(volatile uint32_t* lock);
+static inline void spin_lock(volatile uint32_t SRACY*COUNT(1) lock);
+static inline void spin_unlock(volatile uint32_t SRACY* lock);
 
 /* Inlined functions declared above */
 static inline void atomic_init(atomic_t *number, int32_t val)
index ec42145..2136e6d 100644 (file)
@@ -5,6 +5,10 @@
  * Kevin Klues <klueska@cs.berkeley.edu>    
  */
 
+#ifdef __SHARC__
+#pragma nosharc
+#endif
+
 #include <colored_caches.h>
 
 // Global variables
index 7ba316e..12d5c84 100644 (file)
@@ -37,7 +37,7 @@ void scroll_screen(void);
 #define COM_LSR_DATA   0x01    //   Data available
 #define COM_LSR_READY  0x20    //   Ready to send
 
-static bool serial_exists;
+static bool SREADONLY serial_exists;
 
 int
 serial_proc_data(void)
@@ -47,7 +47,8 @@ serial_proc_data(void)
        return inb(COM1+COM_RX);
 }
 
-int serial_read_byte() {
+int serial_read_byte()
+{
        return serial_proc_data();
 }
 
@@ -80,7 +81,10 @@ serial_init(void)
 
        // Clear any preexisting overrun indications and interrupts
        // Serial port doesn't exist if COM_LSR returns 0xFF
-       serial_exists = (inb(COM1+COM_LSR) != 0xFF);
+       {
+               bool lbool = ((inb(COM1+COM_LSR) != 0xFF));
+               serial_exists = SINIT(lbool);
+       }
        (void) inb(COM1+COM_IIR);
        (void) inb(COM1+COM_RX);
 
@@ -148,30 +152,35 @@ lpt_putc(int c)
 #define MAX_SCROLL_LENGTH      20
 #define SCROLLING_CRT_SIZE     (MAX_SCROLL_LENGTH * CRT_SIZE)
 
-static unsigned addr_6845;
-static uint16_t *COUNT(CRT_SIZE) crt_buf;
-static uint16_t crt_pos;
+static volatile uint32_t SRACY lock = 0;
 
-static uint16_t scrolling_crt_buf[SCROLLING_CRT_SIZE];
-static uint16_t scrolling_crt_pos;
-static uint8_t current_crt_buf;
+static unsigned SREADONLY addr_6845;
+static uint16_t *SLOCKED(&lock) COUNT(CRT_SIZE) crt_buf;
+static uint16_t SLOCKED(&lock) crt_pos;
+
+static uint16_t (SLOCKED(&lock) scrolling_crt_buf)[SCROLLING_CRT_SIZE];
+static uint16_t SLOCKED(&lock) scrolling_crt_pos;
+static uint8_t SLOCKED(&lock) current_crt_buf;
 
 void
 cga_init(void)
 {
-       volatile uint16_t *COUNT(CRT_SIZE) cp;
+       volatile uint16_t SLOCKED(&lock)*COUNT(CRT_SIZE) cp;
        uint16_t was;
        unsigned pos;
 
+       // zra: I suppose this isn't needed, but it makes Ivy shut up
+       //spin_lock_irqsave(&lock);
+
        cp = (uint16_t *COUNT(CRT_SIZE)) TC(KERNBASE + CGA_BUF);
        was = *cp;
        *cp = (uint16_t) 0xA55A;
        if (*cp != 0xA55A) {
                cp = (uint16_t *COUNT(CRT_SIZE)) TC(KERNBASE + MONO_BUF);
-               addr_6845 = MONO_BASE;
+               addr_6845 = SINIT(MONO_BASE);
        } else {
                *cp = was;
-               addr_6845 = CGA_BASE;
+               addr_6845 = SINIT(CGA_BASE);
        }
        
        /* Extract cursor location */
@@ -180,13 +189,16 @@ cga_init(void)
        outb(addr_6845, 15);
        pos |= inb(addr_6845 + 1);
 
-       crt_buf = (uint16_t *COUNT(CRT_SIZE)) cp;
+       crt_buf = (uint16_t SLOCKED(&lock)*COUNT(CRT_SIZE)) cp;
        crt_pos = pos;
        scrolling_crt_pos = 0;
        current_crt_buf = 0;
+
+       //spin_unlock_irqsave(&lock);
 }
 
-static void set_screen(uint8_t screen_num) {
+static void set_screen(uint8_t screen_num)
+{
        uint16_t leftovers = (scrolling_crt_pos % CRT_COLS);
        leftovers = (leftovers) ? CRT_COLS - leftovers : 0;
        
@@ -196,19 +208,22 @@ static void set_screen(uint8_t screen_num) {
        memcpy(crt_buf, scrolling_crt_buf + offset, CRT_SIZE * sizeof(uint16_t));
 }
 
-static void scroll_screen_up(void) {
+static void scroll_screen_up(void)
+{
        if(current_crt_buf <  (scrolling_crt_pos / CRT_SIZE))
                current_crt_buf++;
        set_screen(current_crt_buf);
 }
 
-static void scroll_screen_down(void) {
+static void scroll_screen_down(void)
+{
        if(current_crt_buf > 0) 
                current_crt_buf--;
        set_screen(current_crt_buf);
 }
 
-static void reset_screen(void) {
+static void reset_screen(void)
+{
        current_crt_buf = 0;
        set_screen(current_crt_buf);
 }
@@ -296,7 +311,7 @@ cga_putc(int c)
 
 #define E0ESC          (1<<6)
 
-static uint8_t shiftcode[256] = 
+static uint8_t (SREADONLY shiftcode)[256] = 
 {
        [0x1D] CTL,
        [0x2A] SHIFT,
@@ -306,7 +321,7 @@ static uint8_t shiftcode[256] =
        [0xB8] ALT
 };
 
-static uint8_t togglecode[256] = 
+static uint8_t (SREADONLY togglecode)[256] = 
 {
        [0x3A] CAPSLOCK,
        [0x45] NUMLOCK,
@@ -374,7 +389,7 @@ static uint8_t ctlmap[256] =
        [0xD2] KEY_INS,         [0xD3] KEY_DEL
 };
 
-static uint8_t * COUNT(256) charcode[4] = {
+static uint8_t * COUNT(256) (SREADONLY charcode)[4] = {
        normalmap,
        shiftmap,
        ctlmap,
@@ -385,13 +400,17 @@ static uint8_t * COUNT(256) charcode[4] = {
  * Get data from the keyboard.  If we finish a character, return it.  Else 0.
  * Return -1 if no data.
  */
+#pragma cilnoremove("cons_lock")
+static volatile uint32_t SRACY cons_lock = 0;
+static uint32_t SLOCKED(&cons_lock) shift;
+static bool SLOCKED(&cons_lock) crt_scrolled = FALSE;
+
 static int
 kbd_proc_data(void)
 {
        int c;
        uint8_t data;
-       static uint32_t shift;
-       static bool crt_scrolled = FALSE;
+
 
        if ((inb(KBSTATP) & KBS_DIB) == 0)
                return -1;
@@ -478,12 +497,13 @@ kbd_init(void)
 // whenever the corresponding interrupt occurs.
 
 #define CONSBUFSIZE    512
-
-static struct {
+struct cons {
        uint8_t buf[CONSBUFSIZE];
        uint32_t rpos;
        uint32_t wpos;
-} cons;
+};
+
+static struct cons SLOCKED(&cons_lock) cons;
 
 // called by device interrupt routines to feed input characters
 // into the circular console input buffer.
@@ -507,6 +527,8 @@ cons_getc(void)
 {
        int c;
 
+       spin_lock_irqsave(&cons_lock);
+
        // poll for any pending input characters,
        // so that this function works even when interrupts are disabled
        // (e.g., when called from the kernel monitor).
@@ -520,8 +542,10 @@ cons_getc(void)
                c = cons.buf[cons.rpos++];
                if (cons.rpos == CONSBUFSIZE)
                        cons.rpos = 0;
+               spin_unlock_irqsave(&cons_lock);
                return c;
        }
+       spin_unlock_irqsave(&cons_lock);
        return 0;
 }
 
@@ -529,7 +553,7 @@ cons_getc(void)
 void
 cons_putc(int c)
 {
-       static uint32_t lock;
+       //static uint32_t lock; zra: moving up for sharC annotations
        spin_lock_irqsave(&lock);
        #ifndef SERIAL_IO
                serial_putc(c);
index 4322a98..be253a0 100644 (file)
@@ -4,6 +4,10 @@
  * See LICENSE for details.
  */
 
+#ifdef __SHARC__
+#pragma nosharc
+#endif
+
 #include <arch/arch.h>
 #include <arch/x86.h>
 #include <arch/mmu.h>
@@ -20,7 +24,7 @@ void print_cpuinfo(void)
        uint32_t model, family;
        uint64_t msr_val;
        char vendor_id[13];
-       extern char (SNT _start)[];
+       extern char (SNT SREADONLY _start)[];
 
        asm volatile ("cpuid;"
                  "movl    %%ebx, (%2);"
@@ -97,9 +101,11 @@ void print_cpuinfo(void)
 
 void show_mapping(uintptr_t start, size_t size)
 {
-       pde_t *COUNT(PTSIZE) pgdir = (pde_t *COUNT(PTSIZE))vpd;
-       pte_t *pte, *pde;
-       page_t* page;
+       pde_t SLOCKED(&vpd_lock) *COUNT(PTSIZE) pgdir =
+           (pde_t SLOCKED(&vpd_lock) *COUNT(PTSIZE))vpd;
+       pte_t *pte;
+       pte_t SLOCKED(&vpd_lock) *pde;
+       page_t *page;
        uintptr_t i;
 
        cprintf("   Virtual    Physical  Ps Dr Ac CD WT U W\n");
index 986b96a..33f1d4f 100644 (file)
@@ -1,6 +1,6 @@
 /* See COPYRIGHT for copyright information. */
-#ifdef __DEPUTY__
-#pragma noasync
+#ifdef __SHARC__
+#pragma nosharc
 #endif
 
 #include <arch/trap.h>
index 6f42dce..da4e187 100644 (file)
@@ -5,6 +5,10 @@
  * generates interrupts on IRQ 0.
  */
 
+#ifdef __SHARC__
+#pragma nosharc
+#endif
+
 #include <arch/x86.h>
 
 #include <kclock.h>
index 2b8f098..a2cf1a5 100644 (file)
@@ -1,3 +1,7 @@
+#ifdef __SHARC__
+#pragma nosharc
+#endif
+
 #include <stab.h>
 #include <string.h>
 #include <assert.h>
index 3e6d66f..7687463 100644 (file)
@@ -4,7 +4,11 @@
  * 
  * Kevin Klues <klueska@cs.berkeley.edu>    
  */
+
+#ifdef __SHARC__
+#pragma nosharc
+#endif
+
 #ifdef __DEPUTY__
 #pragma nodeputy
 #endif
index d2db7f8..1293ffd 100644 (file)
@@ -1,3 +1,7 @@
+#ifdef __SHARC__
+#pragma nosharc
+#endif
+
 /* See COPYRIGHT for copyright information. */
 #include <arch/x86.h>
 #include <arch/arch.h>
@@ -22,6 +26,7 @@ pde_t* boot_pgdir;            // Virtual address of boot time page directory
 physaddr_t boot_cr3;           // Physical address of boot time page directory
 
 // Global variables
+volatile uint32_t pages_lock = 0;
 page_t *pages = NULL;          // Virtual address of physical page array
 
 // Global descriptor table.
index 508317b..200c7bb 100644 (file)
@@ -4,6 +4,10 @@
  * See LICENSE for details.
  */
 
+#ifdef __SHARC__
+#pragma nosharc
+#endif
+
 #include <arch/arch.h>
 #include <smp.h>
 
index d842b15..da1a8e7 100644 (file)
@@ -4,6 +4,10 @@
  * See LICENSE for details.
  */
 
+#ifdef __SHARC__
+#pragma nosharc
+#endif
+
 #include <arch/x86.h>
 #include <arch/arch.h>
 #include <smp.h>
@@ -52,7 +56,7 @@ static void init_smp_call_function(void)
 
 /******************************************************************************/
 
-static void smp_mtrr_handler(trapframe_t *tf, barrier_t *data)
+static void ( smp_mtrr_handler)(trapframe_t *tf, barrier_t *data)
 {
        setup_default_mtrrs(data);
 }
index 13439d5..9220afb 100644 (file)
@@ -1,3 +1,6 @@
+#ifdef __SHARC__
+#pragma nosharc
+#endif
 
 #include <arch/mmu.h>
 #include <arch/x86.h>
@@ -31,10 +34,10 @@ pseudodesc_t idt_pd = {
  */
 handler_t TP(void *) interrupt_handlers[NUM_INTERRUPT_HANDLERS];
 
-static const char *NTS (IN_HANDLER trapname)(int trapno)
+static const char *NTS trapname(int trapno)
 {
-    // zra: excnames is NORACE because Ivy doesn't trust const
-       static const char *NT const (NORACE excnames)[] = {
+    // zra: excnames is SREADONLY because Ivy doesn't trust const
+       static const char *NT const ( excnames)[] = {
                "Divide error",
                "Debug",
                "Non-Maskable Interrupt",
@@ -126,7 +129,7 @@ idt_init(void)
 }
 
 void
-(IN_HANDLER print_regs)(push_regs_t *regs)
+print_regs(push_regs_t *regs)
 {
        cprintf("  edi  0x%08x\n", regs->reg_edi);
        cprintf("  esi  0x%08x\n", regs->reg_esi);
@@ -139,7 +142,7 @@ void
 }
 
 void
-(IN_HANDLER print_trapframe)(trapframe_t *tf)
+print_trapframe(trapframe_t *tf)
 {
        cprintf("TRAP frame at %p on core %d\n", tf, core_id());
        print_regs(&tf->tf_regs);
@@ -155,7 +158,7 @@ void
 }
 
 static void
-(IN_HANDLER trap_dispatch)(trapframe_t *tf)
+trap_dispatch(trapframe_t *tf)
 {
        // Handle processor exceptions.
        switch(tf->tf_trapno) {
@@ -191,19 +194,19 @@ static void
 }
 
 void
-(IN_HANDLER env_push_ancillary_state)(env_t* e)
+env_push_ancillary_state(env_t* e)
 {
        // Here's where you'll save FP/MMX/XMM regs
 }
 
 void
-(IN_HANDLER env_pop_ancillary_state)(env_t* e)
+env_pop_ancillary_state(env_t* e)
 {
        // Here's where you'll restore FP/MMX/XMM regs
 }
 
 void
-(IN_HANDLER trap)(trapframe_t *tf)
+trap(trapframe_t *tf)
 {
        //cprintf("Incoming TRAP frame at %p\n", tf);
 
@@ -239,7 +242,7 @@ void
 }
 
 void
-(IN_HANDLER irq_handler)(trapframe_t *tf)
+irq_handler(trapframe_t *tf)
 {
        //if (core_id())
        //      cprintf("Incoming IRQ, ISR: %d on core %d\n", tf->tf_trapno, core_id());
@@ -269,8 +272,8 @@ void
 }
 
 void
-register_interrupt_handler(handler_t TP(TV(t)) table[], uint8_t int_num, poly_isr_t handler,
-                           void* data)
+register_interrupt_handler(handler_t TP(TV(t)) table[],
+                           uint8_t int_num, poly_isr_t handler, void* data)
 {
        table[int_num].isr = handler;
        table[int_num].data = data;
index c98510f..7b25e23 100644 (file)
@@ -10,7 +10,7 @@
 #include <pmap.h>
 
 void
-(IN_HANDLER env_push_ancillary_state)(env_t* e)
+( env_push_ancillary_state)(env_t* e)
 {
        static_assert(offsetof(ancillary_state_t,fpr) % 8 == 0);
 
@@ -46,7 +46,7 @@ void
 }
 
 void
-(IN_HANDLER env_pop_ancillary_state)(env_t* e)
+( env_pop_ancillary_state)(env_t* e)
 { 
 
        #define pop_two_fp_regs(pdest,n) \
index 0dd7574..cbaf19d 100644 (file)
@@ -24,8 +24,8 @@ vm_init(void)
        boot_cr3 = PADDR(boot_pgdir);
 
        size_t env_array_size = ROUNDUP(NENV*sizeof(env_t), PGSIZE);
-       envs = (env_t *)boot_alloc(env_array_size, PGSIZE);
-       memset(envs, 0, env_array_size);
+       envs = /*(env_t *)*/boot_calloc(env_array_size, PGSIZE);
+       //memset(envs, 0, env_array_size);
 }
 
 error_t
index 704ef11..db372af 100644 (file)
@@ -35,7 +35,7 @@ trap_handled(void)
 }
 
 void
-(IN_HANDLER print_trapframe)(trapframe_t *tf)
+( print_trapframe)(trapframe_t *tf)
 {
        int i, len;
        char buf[1024];
index 38cdadb..de94831 100644 (file)
@@ -3,8 +3,9 @@
 #ifndef ROS_INC_ASSERT_H
 #define ROS_INC_ASSERT_H
 
-void _warn(const char* NTS, int, const char* NTS, ...);
-void _panic(const char* NTS, int, const char* NTS, ...) __attribute__((noreturn));
+void ( _warn)(const char* NTS, int, const char* NTS, ...);
+void ( _panic)(const char* NTS, int, const char* NTS, ...)
+    __attribute__((noreturn));
 
 #define warn(...) _warn(__FILE__, __LINE__, __VA_ARGS__)
 #define panic(...) _panic(__FILE__, __LINE__, __VA_ARGS__)
index 975cd1c..d87d3ed 100644 (file)
@@ -6,8 +6,10 @@
 #include <arch/atomic.h>
 #include <arch/arch.h>
 
-static inline void spin_lock_irqsave(volatile uint32_t*SAFE lock);
-static inline void spin_unlock_irqsave(volatile uint32_t*SAFE lock);
+static inline void
+(SLOCK(0) spin_lock_irqsave)(volatile uint32_t SRACY*SAFE lock);
+static inline void
+(SUNLOCK(0) spin_unlock_irqsave)(volatile uint32_t SRACY*SAFE lock);
 
 /*********************** Checklist stuff **********************/
 typedef struct checklist_mask {
index 1bc9822..2f93f79 100644 (file)
@@ -40,6 +40,7 @@ typedef int32_t envid_t;
 #define ENVX(envid)            ((envid) & (NENV - 1))
 
 // TODO: clean this up.
+typedef sharC_env_t;
 struct Env {
        TAILQ_ENTRY(Env) proc_link NOINIT;      // Free list link pointers
        spinlock_t proc_lock;
@@ -54,6 +55,12 @@ struct Env {
        uint32_t env_refcnt;            // Reference count of kernel contexts using this
        uint32_t env_flags;
 
+#ifdef __SHARC__
+       // held spin-locks
+       // zra: Used by Ivy. Let me know if this should go elsewhere.
+       sharC_env_t sharC_env;
+#endif
+
        // Address space
        pde_t *COUNT(NPDENTRIES) env_pgdir;                     // Kernel virtual address of page dir
        physaddr_t env_cr3;                     // Physical address of page dir
@@ -76,7 +83,7 @@ struct Env {
 
 extern env_t *COUNT(NENV) envs;                // All environments
 extern atomic_t num_envs;              // Number of envs
-extern env_t* NORACE curenvs[MAX_NUM_CPUS];
+extern env_t* curenvs[MAX_NUM_CPUS];
 
 void   env_init(void);
 int            env_alloc(env_t *SAFE*SAFE e, envid_t parent_id);
diff --git a/kern/include/ivy/sharc.h b/kern/include/ivy/sharc.h
new file mode 100644 (file)
index 0000000..2b4274b
--- /dev/null
@@ -0,0 +1,171 @@
+#include <assert.h>
+#include <string.h>
+
+#define SINLINE inline
+#define SUNUSED __attribute__((unused))
+
+typedef struct __ivy_sharC_thread {
+#define SHARC_MAX_LOCKS 16
+    void *held_locks[SHARC_MAX_LOCKS];
+    unsigned int max_lock;
+} sharC_env_t;
+
+#include <env.h>
+
+extern int __ivy_checking_on;
+
+#pragma cilnoremove("sharC_env_init")
+static SINLINE void sharC_env_init(sharC_env_t *sharC_env) TRUSTED;
+static SINLINE void sharC_env_init(sharC_env_t *sharC_env)
+WRITES(sharC_env->max_lock,sharC_env->held_locks)
+{
+       sharC_env->max_lock = 0;
+       memset(sharC_env->held_locks,0,SHARC_MAX_LOCKS);
+       return;
+}
+
+#pragma cilnoremove("__sharc_single_threaded")
+static SINLINE void __sharc_single_threaded(void *msg) TRUSTED;
+static SINLINE void __sharc_single_threaded(void *msg)
+{
+       // TODO: how do I know how many threads/cores are running?
+    //assert(1);
+    return;
+}
+
+
+#define GET_SHARC_THREAD() current->sharC_env
+
+#define THREAD_LOCKS(thread,i) (thread.held_locks[(i)])
+#define THREAD_MAX_LOCK(thread) (thread.max_lock)
+
+#define THIS_LOCKS(i)        (THREAD_LOCKS(GET_SHARC_THREAD(),(i)))
+#define THIS_MAX_LOCK        (THREAD_MAX_LOCK(GET_SHARC_THREAD()))
+
+/*
+ * Locks
+ */
+
+extern void
+__sharc_lock_error(const void *lck, const void *what,
+                   unsigned int sz, char *msg);
+
+extern void
+__sharc_lock_coerce_error(void *dstlck, void *srclck, char *msg);
+
+/* assumes no double-locking */
+#pragma cilnoremove("__sharc_add_lock")
+static SINLINE void __sharc_add_lock(void *lck) TRUSTED;
+static SINLINE void __sharc_add_lock(void *lck)
+{
+    unsigned int i;
+
+       if (!__ivy_checking_on || !current) return;
+
+    for (i = 0; i <= THIS_MAX_LOCK; i++)
+        if (!THIS_LOCKS(i))
+            break;
+
+    if (i > THIS_MAX_LOCK && THIS_MAX_LOCK < SHARC_MAX_LOCKS)
+            THIS_MAX_LOCK++;
+
+    THIS_LOCKS(i) = lck;
+    return;
+}
+
+/* this will be very inefficient if the lock isn't actually held */
+#pragma cilnoremove("__sharc_rm_lock")
+static SINLINE void __sharc_rm_lock(void *lck) TRUSTED;
+static SINLINE void __sharc_rm_lock(void *lck)
+{
+    unsigned int i;
+
+       if (!__ivy_checking_on || !current) return;
+
+    for (i = 0; i <= THIS_MAX_LOCK; i++)
+        if (THIS_LOCKS(i) == lck)
+            break;
+
+    if (i == THIS_MAX_LOCK && THIS_MAX_LOCK > 0)
+            THIS_MAX_LOCK--;
+
+    THIS_LOCKS(i) = (void *)0;
+    return;
+}
+
+#pragma cilnoremove("__sharc_chk_lock")
+static SINLINE void
+__sharc_chk_lock(void *lck, void *what, unsigned int sz, char *msg) TRUSTED;
+static SINLINE void
+__sharc_chk_lock(void *lck, void *what, unsigned int sz, char *msg)
+{
+    unsigned int i;
+
+       // TODO: how do I find how many threads are running?
+    //if (__sharc_num_threads == 1) return;
+
+       if (!__ivy_checking_on || !current) return;
+
+    for (i = 0; i <= THIS_MAX_LOCK; i++)
+        if (THIS_LOCKS(i) == lck)
+            break;
+
+    if (i > THIS_MAX_LOCK) {
+            __sharc_lock_error(lck,what,sz,msg);
+    }
+}
+
+#pragma cilnoremove("__sharc_coerce_lock")
+static SINLINE void
+__sharc_coerce_lock(void *dstlck, void *srclck, char *msg) TRUSTED;
+static SINLINE void
+__sharc_coerce_lock(void *dstlck, void *srclck, char *msg)
+{
+       if (!__ivy_checking_on) return;
+
+    if (dstlck != srclck)
+        __sharc_lock_coerce_error(dstlck,srclck,msg);
+}
+
+/*
+ * The sharing cast.
+ *
+ */
+
+extern void __sharc_group_cast_error(int, void *, void *, char *);
+
+#pragma cilnoremove("__sharc_check_group_cast")
+static inline void
+__sharc_check_group_cast(int hassame, void *srcg, void *src, char *msg) TRUSTED;
+static inline void
+__sharc_check_group_cast(int hassame, void *srcg, void *src, char *msg)
+{
+       int old;
+       if (!__ivy_checking_on) return;
+       old = __ivy_checking_on;
+       __ivy_checking_on = 0;
+       panic("sharc group cast unimplemented");
+       __ivy_checking_on = old;
+}
+
+
+extern void __sharc_cast_error(void *addr, unsigned long sz, char *msg);
+
+#pragma cilnoremove("__sharc_sharing_cast")
+static SINLINE void *
+__sharc_sharing_cast(void *addr,void **slot, unsigned int localslot SUNUSED,
+                     unsigned long lo, unsigned long hi,
+                     char *msg) TRUSTED;
+static SINLINE void *
+__sharc_sharing_cast(void *addr,void **slot, unsigned int localslot SUNUSED,
+                     unsigned long lo, unsigned long hi,
+                     char *msg)
+{
+       int old;
+       if (!__ivy_checking_on) return NULL;
+       old = __ivy_checking_on;
+       __ivy_checking_on = 0;
+       panic("sharc sharing cast unimplemented");
+       __ivy_checking_on = old;
+       return NULL;
+}
index 8d7af4c..f705e87 100644 (file)
@@ -7,7 +7,7 @@
 // Activate the kernel monitor,
 // optionally providing a trap frame indicating the current state
 // (NULL if none).
-void (IN_HANDLER monitor)(trapframe_t *tf);
+void ( monitor)(trapframe_t *tf);
 
 // Functions implementing monitor commands.
 int mon_help(int argc, char *NTS *NT COUNT(argc) argv, trapframe_t *tf);
index c6d4569..e59d218 100644 (file)
@@ -41,7 +41,9 @@
 
 extern char (SNT bootstacktop)[], (SNT bootstack)[];
 
-extern page_t *COUNT(npages) pages; // List of pysical pages
+// List of pysical pages
+extern volatile uint32_t pages_lock;
+extern page_t SLOCKED(&pages_lock) * SREADONLY COUNT(npages) pages;
 
 extern physaddr_t boot_cr3;
 extern pde_t *COUNT(NPDENTRIES) boot_pgdir;
@@ -59,7 +61,7 @@ int       page_insert(pde_t *COUNT(NPDENTRIES) pgdir, page_t *pp, void *SNT va, in
 void*COUNT(PGSIZE) page_insert_in_range(pde_t *COUNT(NPDENTRIES) pgdir, page_t *pp, 
                              void *SNT vab, void *SNT vae, int perm);
 void   page_remove(pde_t *COUNT(NPDENTRIES) pgdir, void *SNT va);
-page_t*COUNT(1) page_lookup(pde_t *COUNT(NPDENTRIES) pgdir, void *SNT va, pte_t **pte_store);
+page_t*COUNT(1) page_lookup(pde_t SSOMELOCK*COUNT(NPDENTRIES) pgdir, void *SNT va, pte_t **pte_store);
 error_t        pagetable_remove(pde_t *COUNT(NPDENTRIES) pgdir, void *SNT va);
 void   page_decref(page_t *COUNT(1) pp);
 
index 5f7868a..ee2bcb7 100644 (file)
@@ -39,8 +39,8 @@ int proc_set_state(struct proc *p, uint32_t state) WRITES(p->state);
 struct proc *get_proc(unsigned pid);
 bool proc_controls(struct proc *actor, struct proc *target);
 void proc_run(struct proc *p);
-void proc_startcore(struct proc *p, trapframe_t *tf) __attribute__((noreturn));
-void proc_destroy(struct proc *SAFE p);
+void (proc_startcore)(struct proc *p, trapframe_t *tf) __attribute__((noreturn));
+void (proc_destroy)(struct proc *SAFE p);
 
 /* The reference counts are mostly to track how many cores loaded the cr3 */
 error_t proc_incref(struct proc *SAFE p);
index d40ab7e..38c521e 100644 (file)
 typedef uint32_t pte_t;
 typedef uint32_t pde_t;
 
-extern volatile pte_t (COUNT(PTSIZE) vpt)[];     // VA of "virtual page table"
-extern volatile pde_t (COUNT(PTSIZE) vpd)[];     // VA of current page directory
+#pragma cilnoremove("vpt_lock", "vpd_lock")
+extern volatile uint32_t vpt_lock;
+extern volatile uint32_t vpd_lock;
+
+extern volatile pte_t SLOCKED(&vpt_lock) (COUNT(PTSIZE) SREADONLY vpt)[]; // VA of "virtual page table"
+extern volatile pde_t SLOCKED(&vpd_lock) (COUNT(PTSIZE) SREADONLY vpd)[]; // VA of current page directory
 
 #endif /* !__ASSEMBLER__ */
 #endif /* !ROS_INC_MEMLAYOUT_H */
index 8d2e6ae..8212951 100644 (file)
@@ -31,7 +31,7 @@ void  vprintfmt(void (*putch)(int, void**), void **putdat, const char *NTS fmt, v
 #endif
 
 // lib/printf.c
-int    cprintf(const char * NTS fmt, ...);
+int    ( cprintf)(const char * NTS fmt, ...);
 int    vcprintf(const char * NTS fmt, va_list);
 
 // lib/sprintf.c
index 5677a99..17dc62d 100644 (file)
@@ -7,7 +7,7 @@
 #include <ros/syscall.h>
 #include <process.h>
 
-int32_t (SYNCHRONOUS syscall)(env_t* e, uint32_t num, uint32_t a1, uint32_t a2,
+int32_t (syscall)(env_t* e, uint32_t num, uint32_t a1, uint32_t a2,
                               uint32_t a3, uint32_t a4, uint32_t a5);
 int32_t syscall_async(env_t* e, syscall_req_t *syscall);
 int32_t process_generic_syscalls(env_t* e, uint32_t max);
index 455bbb8..9931c77 100644 (file)
@@ -10,7 +10,7 @@
 #include <arch/trap.h>
 
 // func ptr for interrupt service routines
-typedef void (*poly_isr_t)(trapframe_t* tf, TV(t) data);
+typedef void ( *poly_isr_t)(trapframe_t* tf, TV(t) data);
 typedef void (*isr_t)(trapframe_t* tf, void * data);
 typedef struct InterruptHandler {
        poly_isr_t isr;
@@ -20,8 +20,8 @@ typedef struct InterruptHandler {
 void idt_init(void);
 void register_interrupt_handler(handler_t (COUNT(256)table)[], uint8_t int_num,
                                 poly_isr_t handler, TV(t) data);
-void (IN_HANDLER print_trapframe)(trapframe_t *tf);
-void (IN_HANDLER page_fault_handler)(trapframe_t *tf);
+void ( print_trapframe)(trapframe_t *tf);
+void ( page_fault_handler)(trapframe_t *tf);
 
 void sysenter_init(void);
 extern void sysenter_handler();
index fa62c72..aaee01f 100644 (file)
@@ -1,8 +1,8 @@
 KERN_IVY_DIR = $(KERN_DIR)/ivy\r
 OBJDIRS += $(KERN_IVY_DIR)\r
 \r
-KERN_IVY_CFLAGS   := $(KERN_CFLAGS) --nodeputy\r
-KERN_IVY_SRCFILES := $(KERN_IVY_DIR)/deputy.c\r
+KERN_IVY_CFLAGS   := $(KERN_CFLAGS) --nodeputy --nosharc\r
+KERN_IVY_SRCFILES := $(KERN_IVY_DIR)/deputy.c $(KERN_IVY_DIR)/sharc.c\r
 KERN_IVY_OBJFILES := $(patsubst $(KERN_IVY_DIR)/%.c, \\r
                                    $(OBJDIR)/$(KERN_IVY_DIR)/%.o, \\r
                                    $(KERN_IVY_SRCFILES))\r
index 9747f1f..87c568c 100644 (file)
 #define noreturn __attribute__((noreturn))
 #endif
 
+extern int __ivy_checking_on;
+
 asmlinkage
 void deputy_fail_mayreturn(const char *check, const char *text,
                            __LOCATION__FORMALS) {
+       int old;
+       if (!__ivy_checking_on) return;
+       old = __ivy_checking_on;
+       __ivy_checking_on = 0;
     cprintf("%s:%d: %s: Assertion failed in %s: %s\n",
             __LOCATION__ACTUALS, check, text);
+       __ivy_checking_on = old;
 /*
     dump_stack();
 */
@@ -36,7 +43,9 @@ void deputy_fail_mayreturn(const char *check, const char *text,
 
 asmlinkage noreturn
 void deputy_fail_noreturn_fast(void) {
+       __ivy_checking_on = 0;
     panic("Deputy assertion failure\n");
+       __ivy_checking_on = 1;
 }
 
 int deputy_strlen(const char *str) {
@@ -86,7 +95,10 @@ int deputy_findnull(const void *e, unsigned int bytes) {
             NULLCHECK(long);
             break;
         default:
+                       if (!__ivy_checking_on) return length;
+                       __ivy_checking_on = 0;
             cprintf("Invalid byte size for nullcheck.\n");
+                       __ivy_checking_on = 1;
             break;
     }
 
@@ -98,14 +110,3 @@ void *__deputy_memset(void *s, int c, unsigned int n) {
   return memset(s, c, n);
 }
 
-void __ivy_handler_atomic_entry() __attribute__((weak));
-void __ivy_handler_atomic_entry() {return;}
-
-void __ivy_handler_atomic_exit() __attribute__((weak));
-void __ivy_handler_atomic_exit() {return;}
-
-void __ivy_handler_atomic_locks_entry(unsigned int n, ...) __attribute__((weak));
-void __ivy_handler_atomic_locks_entry(unsigned int n, ...) {return;}
-
-void __ivy_handler_atomic_locks_exit(unsigned int n, ...) __attribute__((weak));
-void __ivy_handler_atomic_locks_exit(unsigned int n, ...) {return;}
diff --git a/kern/ivy/sharc.c b/kern/ivy/sharc.c
new file mode 100644 (file)
index 0000000..17f09a0
--- /dev/null
@@ -0,0 +1,25 @@
+#include <assert.h>
+
+int __ivy_checking_on = 1;
+
+void __sharc_lock_error(const void *lck, const void *what,
+                        unsigned int sz, char *msg)
+{
+       int old;
+       if (!__ivy_checking_on) return;
+       old = __ivy_checking_on;
+       __ivy_checking_on = 0;
+       warn("Ivy: The lock %p was not held for (%p,%d): %s\n",
+          lck, what, sz, msg);
+       __ivy_checking_on = old;
+}
+
+void __sharc_lock_coerce_error(void *dstlck, void *srclck, char *msg)
+{
+       int old;
+       if (!__ivy_checking_on) return;
+       old = __ivy_checking_on;
+       __ivy_checking_on = 0;
+       warn("Ivy: The locks in the coercion at %s must be the same\n", msg);
+       __ivy_checking_on = old;
+}
index b1d705e..47c44ac 100644 (file)
@@ -1,3 +1,7 @@
+#ifdef __SHARC__
+#pragma nosharc
+#endif
+
 #include <arch/arch.h>
 
 #include <atomic.h>
index 107271e..307c30d 100644 (file)
@@ -5,6 +5,10 @@
  * Kevin Klues <klueska@cs.berkeley.edu>    
  */
 
+#ifdef __SHARC__
+#pragma nosharc
+#endif
+
 #include <arch/types.h>
 #include <arch/mmu.h>
 #include <colored_caches.h>
index 4413a65..b063137 100644 (file)
@@ -1,5 +1,9 @@
 /* See COPYRIGHT for copyright information. */
 
+#ifdef __SHARC__
+#pragma nosharc
+#endif
+
 #include <arch/arch.h>
 #include <arch/mmu.h>
 #include <elf.h>
@@ -90,12 +94,13 @@ env_init(void)
        atomic_init(&num_envs, 0);
        TAILQ_INIT(&proc_freelist);
        assert(envs != NULL);
-       for (i = NENV-1; i >= 0; i--) { TRUSTEDBLOCK // asw ivy workaround
+       for (i = NENV-1; i >= 0; i--) {
                // these should already be set from when i memset'd the array to 0
                envs[i].state = ENV_FREE;
                envs[i].env_id = 0;
                TAILQ_INSERT_HEAD(&proc_freelist, &envs[i], proc_link);
        }
+
 }
 
 //
@@ -266,6 +271,10 @@ env_alloc(env_t **newenv_store, envid_t parent_id)
        e->env_refcnt = 1;
        e->env_flags = 0;
 
+#ifdef __SHARC__
+       /* init SharC state */
+       sharC_env_init(&e->sharC_env);
+#endif
 
        memset(&e->env_ancillary_state, 0, sizeof(e->env_ancillary_state));
        memset(&e->env_tf, 0, sizeof(e->env_tf));
@@ -455,6 +464,18 @@ env_free(env_t *e)
        TAILQ_INSERT_HEAD(&proc_freelist, e, proc_link);
 }
 
+
+#define PER_CPU_THING(type,name)\
+type SLOCKED(name##_lock) * RWPROTECT name;\
+type SLOCKED(name##_lock) *\
+(get_per_cpu_##name)()\
+{\
+       { R_PERMITTED(global(name))\
+               return &name[core_id()];\
+       }\
+}
+
+
 /* This is the top-half of an interrupt handler, where the bottom half is
  * proc_run (which never returns).  Just add it to the delayed work queue,
  * which (incidentally) can only hold one item at this point.
@@ -466,7 +487,7 @@ void run_env_handler(trapframe_t *tf, env_t *data)
        assert(data);
        struct work TP(env_t *) job;
        struct workqueue *workqueue = &per_cpu_info[core_id()].workqueue;
-       { //TRUSTEDBLOCK TODO: how do we make this func_t cast work?
+       {
        job.func = proc_run;
        job.data = data;
        }
index ba518a1..8b74c2d 100644 (file)
@@ -1,5 +1,9 @@
 /* See COPYRIGHT for copyright information. */
 
+#ifdef __SHARC__
+#pragma nosharc
+#endif
+
 #ifdef __BSD_ON_CORE_0__
 #include Everything For Free -- It just works!!
 #else
index 72a3f3b..5df42c7 100644 (file)
@@ -4,6 +4,10 @@
  * See LICENSE for details.
  */
 
+#ifdef __SHARC__
+#pragma nosharc
+#endif
+
 #include <kfs.h>
 #include <string.h>
 #include <assert.h>
index ba321f1..8d3b72b 100644 (file)
@@ -5,6 +5,10 @@
  * Kevin Klues <klueska@cs.berkeley.edu>    
  */
 
+#ifdef __SHARC__
+#pragma nosharc
+#endif
+
 #include <arch/types.h>
 #include <ros/error.h>
 #include <pmap.h>
index 7f88665..1748662 100644 (file)
@@ -4,6 +4,10 @@
  * See LICENSE for details.
  */
 
+#ifdef __SHARC__
+#pragma nosharc
+#endif
+
 #include <arch/types.h>
 #include <smp.h>
 
index 9b87344..f664e47 100644 (file)
@@ -1,6 +1,10 @@
 // Simple command-line kernel monitor useful for
 // controlling the kernel and exploring the system interactively.
 
+#ifdef __SHARC__
+#pragma nosharc
+#endif
+
 #include <arch/arch.h>
 #include <stab.h>
 #include <smp.h>
index f6e937f..ece4831 100644 (file)
@@ -1,3 +1,7 @@
+#ifdef __SHARC__
+#pragma nosharc
+#endif
+
 #include <multiboot.h>
 #include <arch/types.h>
 #include <arch/mmu.h>
index 93cd9c8..ac4831b 100644 (file)
@@ -5,6 +5,10 @@
  * Kevin Klues <klueska@cs.berkeley.edu>    
  */
 
+#ifdef __SHARC__
+#pragma nosharc
+#endif
+
 #include <sys/queue.h>
 #include <page_alloc.h>
 #include <pmap.h>
index bada5d0..2b240b6 100644 (file)
  * @author Barret Rhoden <brho@cs.berkeley.edu>
  */
 
+#ifdef __SHARC__
+#pragma nosharc
+#endif
+
 #include <arch/arch.h>
 #include <arch/mmu.h>
 
@@ -31,6 +35,9 @@
  */
 static void *DANGEROUS user_mem_check_addr;
 
+volatile uint32_t vpt_lock = 0;
+volatile uint32_t vpd_lock = 0;
+
 /**
  * @brief Initialize the array of physical pages and memory free list.
  *
index e870dca..df4677f 100644 (file)
@@ -1,6 +1,10 @@
 // Simple implementation of cprintf console output for the kernel,
 // based on printfmt() and the kernel console's cputchar().
 
+#ifdef __SHARC__
+#pragma nosharc
+#endif
+
 #include <arch/arch.h>
 #include <arch/types.h>
 
index 5d4fc83..e25df34 100644 (file)
@@ -2,6 +2,10 @@
 // used in common by printf, sprintf, fprintf, etc.
 // This code is also used by both the kernel and user programs.
 
+#ifdef __SHARC__
+#pragma nosharc
+#endif
+
 #include <arch/types.h>
 #include <ros/error.h>
 #include <stdio.h>
index 616aa64..39c47a6 100644 (file)
@@ -4,6 +4,10 @@
  * See LICENSE for details.
  */
 
+#ifdef __SHARC__
+#pragma nosharc
+#endif
+
 #include <process.h>
 #include <atomic.h>
 #include <smp.h>
index 71a46c6..fc26f46 100644 (file)
@@ -1,4 +1,8 @@
 
+#ifdef __SHARC__
+#pragma nosharc
+#endif
+
 #include <ros/error.h>
 #include <stdio.h>
 
index a4ff0c7..ec3cc49 100644 (file)
@@ -6,6 +6,10 @@
  * Scheduling and dispatching.
  */
 
+#ifdef __SHARC__
+#pragma nosharc
+#endif
+
 #include <schedule.h>
 #include <process.h>
 #include <monitor.h>
index c1cdc0e..aa50ac5 100644 (file)
@@ -4,6 +4,10 @@
  * See LICENSE for details.
  */
 
+#ifdef __SHARC__
+#pragma nosharc
+#endif
+
 #include <arch/arch.h>
 #include <atomic.h>
 #include <smp.h>
index e73f98f..8d3a8ca 100644 (file)
@@ -1,5 +1,9 @@
 // Basic string routines.  Not hardware optimized, but not shabby.
 
+#ifdef __SHARC__
+#pragma nosharc
+#endif
+
 #include <string.h>
 
 int
index ec9b0fd..8419a7a 100644 (file)
@@ -1,5 +1,9 @@
 /* See COPYRIGHT for copyright information. */
 
+#ifdef __SHARC__
+#pragma nosharc
+#endif
+
 #include <arch/types.h>
 #include <arch/arch.h>
 #include <arch/mmu.h>
index f67e3ce..a6ce6fb 100644 (file)
@@ -4,4 +4,7 @@
  * 
  * Kevin Klues <klueska@cs.berkeley.edu>    
  */
+
+#ifdef __SHARC__
+#pragma nosharc
+#endif
index bc6060c..a0edd20 100644 (file)
@@ -1,4 +1,8 @@
 
+#ifdef __SHARC__
+#pragma nosharc
+#endif
+
 #include <arch/mmu.h>
 #include <arch/arch.h>
 #include <smp.h>
index 48fdec4..d3eeeee 100644 (file)
@@ -1,3 +1,8 @@
+
+#ifdef __SHARC__
+#pragma nosharc
+#endif
+
 #include <arch/arch.h>
 #include <ros/timer.h>
 
index 5e2de2f..b88907c 100644 (file)
@@ -4,6 +4,10 @@
  * See LICENSE for details.
  */
 
+#ifdef __SHARC__
+#pragma nosharc
+#endif
+
 #include <atomic.h>
 #include <smp.h>
 
index 0596f5e..5eeb0a3 100644 (file)
@@ -1,6 +1,6 @@
 USER_DIR = user
 
-USER_CFLAGS  := $(CFLAGS) -DROS_USER 
+USER_CFLAGS  := $(USER_IVY_FLAGS) $(CFLAGS) -DROS_USER 
 USER_LDFLAGS := $(LDFLAGS)
 
 include $(USER_DIR)/roslib/Makefrag